+
+'''''
+
+_Teaching systems thinking through computational haptics. Learn by
+feeling the code._ 📚✨
diff --git a/README.md b/README.md
deleted file mode 100644
index 8da91d6..0000000
--- a/README.md
+++ /dev/null
@@ -1,437 +0,0 @@
-
-
-[](https://github.com/hyperpolymath/palimpsest-license) 
-
-
-
-
-**A pedagogical programming language where the language itself is
-intentionally fragile** with built-in contradictions and paradoxes.
-
-
-
-Error-Lang makes programming learnable the way crafts are learnable -
-through direct feedback, exploration, and developing an intuitive feel
-for the computational substrate.
-
-
-
-# Status: Production-Ready (100%)
-
-**Integration Complete** — All core components implemented, tested, and
-formally verified (2026-02-07)
-
-| Component | Status | Description |
-|----|----|----|
-| **Compiler & Runtime** | ✅ 100% | AffineScript compiler with lexer, parser, type checker, analyzer (7,468 LOC base) |
-| **Bytecode VM** | ✅ 100% | Stack-based interpreter with positional semantics and computational haptics (520 LOC) |
-| **Codegen** | ✅ 100% | AST to bytecode compiler with position metadata preservation (425 LOC) |
-| **Zig FFI** | ✅ 100% | High-performance computational haptics (stability scoring, paradox detection, 450 LOC) |
-| **LSP Server** | ✅ 100% | Language Server Protocol with real-time stability tracking (310 LOC) |
-| **VS Code Extension** | ✅ 100% | Syntax highlighting, LSP integration, computational haptics visualization |
-| **Documentation** | ✅ 100% | Language spec, tutorials (10 levels), API docs, pedagogy guide |
-| **Deployment** | ✅ 100% | Svalinn/Vordr verified container stack with formal verification |
-
-# What is Error-Lang?
-
-Unlike traditional teaching languages that hide complexity, Error-Lang
-**exposes complexity** and makes it explorable through **computational
-haptics** - visual feedback that lets you *feel* code quality like a
-craftsperson feels their materials.
-
-Error-Lang is a **dissembling**, **decompositional** language: programs,
-syntax, semantics, and types can decay, decompose, and destabilise over
-time — and the language makes that decomposition **visible** rather than
-hiding it. Its `Echo` types give **structured loss** a first-class shape
-(`Echo` retained witness + visible output; `EchoR` the
-non-recoverable residue after `echo_to_residue`, which debits
-stability). The governing rule is **decomposition must be visible**. See
-`docs/Echo-Decomposition.adoc`.
-
-## The Craftsperson Analogy
-
-> A master carpenter feels the weight of their hammer and adjusts their
-> swing. A skilled cook sees the vortex in boiling water and knows when
-> to add pasta. A sculptor feels stone resistance and knows where it
-> will crack.
->
-> **If craftspeople can develop this intuition for simple materials,
-> imagine the potential in understanding syntax, semantics, and
-> typing.**
->
-> — The Design Philosophy
-
-# Quick Start
-
-## Installation
-
-```bash
-# Clone the repository
-git clone https://github.com/hyperpolymath/error-lang.git
-cd error-lang
-
-# Install Deno (if not already installed)
-curl -fsSL https://deno.land/install.sh | sh
-
-# Run an example
-deno run -A cli/runtime.js examples/01-hello-world.err
-```
-
-## Your First Program
-
-``` error-lang
-# examples/01-hello-world.err
-main
- println("Hello, Error-Lang!")
- let x = 42
- println("Stability score:", stability())
-end
-```
-
-Run it:
-
-```bash
-deno run -A cli/runtime.js examples/01-hello-world.err
-```
-
-Output: \`\`\` Hello, Error-Lang! Stability score: 100
-
-✨ \[████████████████████\] 100/100 Stability: EXCELLENT \`\`\`
-
-## Your First Paradox (Positional Semantics)
-
-``` error-lang
-# The + operator behavior depends on its column position!
-main
- let a = 5 + 3 # Column 12 (even): Addition → 8
- let b = 5 + 3 # Column 12 (even): Addition → 8
- let c = 5 + 3 # Column 13 (odd): Concatenation → "53"
-
- println(a, b, c) # 8, 8, "53"
-end
-```
-
-**The paradox:** Moving one space changes operator behavior!
-
-```bash
-deno run -A cli/runtime.js examples/02-positional-operators.err
-
-# Watch the stability score drop as you discover the paradox
-💫 [█████████████░░░░░░░] 65/100
-Stability: FAIR
-Factors: positional-semantics
-```
-
-# Core Concepts
-
-## Computational Haptics
-
-Visual feedback that makes design decisions immediately tangible:
-
-- **Animated stability bar** - Real-time updates (0-100 score)
-
-- **Color coding** - Green → Yellow → Orange → Red
-
-- **Emoji indicators** - ✨ → 💫 → ⚠️ → 🔥
-
-- **Sparkline history** - Trend visualization
-
-- **IDE integration** - Real-time VS Code overlay
-
-## The Ten Paradoxes
-
-Error-Lang has ten core paradoxes that challenge assumptions:
-
-1. **Type Quantum Superposition** - Variables exist in multiple types
- until observed
-
-2. **Scope Leakage** - Variables escape blocks on prime-numbered lines
-
-3. **Positional Operator Semantics** - Operators change behavior by
- file position
-
-4. **Context-Collapse Keywords** - `maybe`, `sometimes`, `usually`
- affect semantics
-
-5. **Temporal Corruption** - Previous run history affects current
- execution
-
-6. **Reserved Word Roulette** - Keywords shift meaning based on context
-
-7. **Arithmetic Drift** - Math operations have small, accumulating
- errors
-
-8. **Null Propagation Cascade** - Null spreads like a virus
-
-9. **Global State Entanglement** - Globals affect each other
- mysteriously
-
-10. **Memory Phantom** - Freed memory sometimes persists
-
-See Paradoxes for
-detailed examples.
-
-## Five Abstraction Layers
-
-Navigate code through five transformation layers:
-
- Grammar ←→ EBNF rules that matched
- ↓
- Parser ←→ Concrete syntax tree
- ↓
- AST ←→ Abstract syntax tree
- ↓
- Semantics ←→ Type-checked, analyzed AST
- ↓
- Runtime ←→ Execution trace
-
-The IDE lets you explore each layer and see exactly where paradoxes
-emerge.
-
-## Five Whys Root Cause Analysis
-
-Automated root cause tracing from symptom to design decision:
-
- Why? Compiler rejected code
- Why? Type mismatch detected
- Why? Type superposition active
- Why? Too many variables in scope (>10)
- Why? Scope leakage on line 7 (prime number)
- ROOT: Positional semantics paradox
-
-# Development Tools
-
-## CLI Tools
-
-```bash
-# Run program
-deno run -A cli/runtime.js program.err
-
-# Analyze stability
-deno run -A cli/analyze.js program.err
-
-# Five Whys analysis
-deno run -A cli/five-whys.js program.err
-
-# Layer navigation
-deno run -A cli/layer-navigator.js program.err
-
-# Visual feedback
-deno run -A cli/visual-feedback.js program.err
-```
-
-## LSP Server
-
-```bash
-# Start LSP server for IDE integration (built into the AffineScript compiler)
-affinescript server
-```
-
-Features: - Real-time diagnostics with paradox warnings - Hover info
-showing stability scores - Auto-completion for keywords and built-ins -
-Custom stability notifications for UI
-
-## VS Code Extension
-
-Install from `vscode-extension/`:
-
-```bash
-cd vscode-extension
-npm install
-npm run compile
-npm run package
-code --install-extension error-lang-1.0.0.vsix
-```
-
-Features: - Syntax highlighting for `.err` files - Special highlighting
-for positional operators - LSP integration - Real-time computational
-haptics overlay
-
-# Bytecode VM
-
-Error-Lang compiles to bytecode for portable execution:
-
-```bash
-# Compile to bytecode
-deno run -A compiler/compile.js program.err -o program.bc
-
-# Run bytecode
-deno run -A compiler/vm.js program.bc
-
-# Disassemble bytecode
-deno run -A compiler/disassemble.js program.bc
-```
-
-The VM preserves positional semantics and tracks computational haptics
-during execution.
-
-# Formal Verification
-
-Error-Lang integrates with:
-
-- **Idris2**: ABI proofs for FFI safety (`src/abi/*.idr`)
-
-- **Zig**: Memory-safe FFI implementation (`ffi/zig/`)
-
-- **Vörðr**: Runtime verification with formal proofs
-
-Verified properties: - ✓ Stability scores bounded \[0, 100\] - ✓
-Positional operator behavior deterministic - ✓ Paradox detection
-monotonic with complexity
-
-# Deployment
-
-## Svalinn/Vordr Stack (Recommended)
-
-```bash
-# Build with formal verification
-svalinn-compose build
-
-# Deploy all services (LSP + VM + IDE)
-svalinn-compose up
-
-# Scale on-demand
-svalinn-compose up --scale vm-runtime=3
-```
-
-See svalinn-compose for
-full configuration.
-
-Services: - **LSP Server** (2 replicas) - Language server for IDE
-integration - **VM Runtime** (on-demand) - Bytecode execution with
-haptics - **IDE/Playground** - Web-based development environment
-
-## Standalone Container
-
-```bash
-podman build -f Containerfile -t error-lang:latest .
-podman run -p 8080:8080 error-lang:latest
-```
-
-# Documentation
-
-- [Language Specification](docs/LANGUAGE-SPEC.md) - Complete grammar and
- semantics
-
-- [Tutorial](docs/TUTORIAL.md) - 10 step-by-step lessons
-
-- [Paradoxes](docs/Paradoxes.adoc) - All 10 paradoxes explained
-
-- [Examples](examples/) - 16+ example programs
-
-- [Completion Report](ERROR-LANG-COMPLETION-2026-02-07.md) - Full
- development history
-
-# Architecture
-
- ┌────────────────────────────────────────────────────┐
- │ Error-Lang Architecture │
- ├────────────────────────────────────────────────────┤
- │ │
- │ ┌──────────┐ ┌──────────┐ │
- │ │ Source │──────▶│ Parser │ │
- │ │ (.err) │ │ (ReS) │ │
- │ └──────────┘ └────┬─────┘ │
- │ │ │
- │ ▼ │
- │ ┌──────────┐ │
- │ │ AST │ │
- │ └────┬─────┘ │
- │ │ │
- │ ┌──────────────┼──────────────┐ │
- │ ▼ ▼ ▼ │
- │ ┌─────────┐ ┌──────────┐ ┌─────────┐ │
- │ │Analyzer │ │ Codegen │ │ REPL │ │
- │ │(Haptics)│ │(Bytecode)│ │ │ │
- │ └─────────┘ └────┬─────┘ └─────────┘ │
- │ │ │
- │ ▼ │
- │ ┌─────────┐ │
- │ │ VM │ │
- │ │ (Stack) │ │
- │ └────┬────┘ │
- │ │ │
- │ ▼ │
- │ ┌────────────────┐ │
- │ │ Computational │ │
- │ │ Haptics │ │
- │ │ (Zig FFI) │ │
- │ └────────────────┘ │
- │ │
- ├────────────────────────────────────────────────────┤
- │ Tooling: LSP | VS Code | Debugger | Profiler │
- └────────────────────────────────────────────────────┘
-
-# Use Cases
-
-Ideal for: - **Computer science education** - Teaching systems
-thinking - **Debugging and error handling** - Understanding failure
-modes - **Language design courses** - Exploring trade-offs - **Code
-quality awareness** - Developing intuition - **Pedagogical research** -
-Studying learning through mistakes
-
-# Project Statistics
-
-| Metric | Value |
-|----|----|
-| Lines of Code | 9,200+ |
-| Files | 38 |
-| Languages | AffineScript (21 files), Idris2 (6 files), Zig (3 files), TypeScript (1 file) |
-| Completion | 100% |
-| Test Coverage | Core components tested (14 Zig FFI tests passing) |
-| Documentation | Complete (spec + 10 tutorials + API docs) |
-| Container Size | ~80MB (multi-stage build) |
-
-# Contributing
-
-See CONTRIBUTING for
-development guidelines.
-
-**Code of Conduct**:
-CODE_OF_CONDUCT
-
-# License
-
-SPDX-License-Identifier: CC-BY-SA-4.0
-
-Error-Lang is free software under the
-MPL-2 (MPL-2.0).
-
-See [LICENSE](LICENSE) for full terms.
-
-# Related Projects
-
-- [Svalinn](https://github.com/hyperpolymath/svalinn) - Edge gateway for
- verified containers
-
-- [Vörðr](https://github.com/hyperpolymath/vordr) - Formally verified
- container runtime
-
-- [Selur](https://github.com/hyperpolymath/selur) - Zero-copy WASM
- bridge
-
-- [NextGen
- Languages](https://github.com/hyperpolymath/nextgen-languages) -
- Language portfolio
-
-# Contact
-
-- **Issues**:
-
-- **Discussions**:
-
-
-- **Author**: Jonathan D.A. Jewell
- \<[j.d.a.jewell@open.ac](j.d.a.jewell@open.ac).uk\>
-
-------------------------------------------------------------------------
-
-*Teaching systems thinking through computational haptics. Learn by
-feeling the code.* 📚✨
diff --git a/REQUIRES_INITIALISATION.adoc b/REQUIRES_INITIALISATION.adoc
new file mode 100644
index 0000000..456ef6c
--- /dev/null
+++ b/REQUIRES_INITIALISATION.adoc
@@ -0,0 +1,84 @@
+== REQUIRES INITIALISATION
+
+*This repository is not finished being set up.* 4 substitution token(s)
+across 2 file(s) still have no value.
+
+=== Why this is not already done
+
+This repo was created from `+hyperpolymath/rsr-template-repo+`. The mint
+(`+just repo-init+`) fills every token that has a single mechanical
+answer — owner, repo, author, dates, licence, branch — and it has done
+so here.
+
+The tokens below are the ones it _deliberately cannot_ answer. They need
+a decision or a fact that exists only in your head: what this project is
+for, what command builds it, which port the service listens on, whether
+a PGP key is held at all. The template’s own token vocabulary says as
+much — you cannot sensibly answer "`required invariants`" in a
+thirty-second bootstrap.
+
+They were left *visibly unfilled on purpose*. The alternatives were both
+worse: inventing plausible values would put confident falsehoods into a
+security policy and an architecture document, and silently deleting the
+sections would hide the fact that a decision is owed. A visible gap is
+honest; a fabricated answer is not.
+
+=== Do not delete this file until every item below is resolved
+
+This file is the only marker that the work is outstanding. Deleting it
+early does not finish the setup, it just conceals it — and the next
+person or agent to arrive will reasonably assume the repo is complete.
+
+* *If you are a person:* delete this file yourself once the last item is
+done.
+* *If you are an agent:* resolve what you legitimately can, leave the
+rest, and delete this file only when no token below remains anywhere in
+the tree. Do not delete it to make a gate go green.
+
+Re-running the estate top-up tool will remove this file automatically
+once nothing is outstanding, so the safest way to finish is to fix the
+tokens and let the check confirm it.
+
+=== What is needed, and where it goes
+
+==== `+{{CONDUCT_TEAM}}+`
+
+Name of the conduct body. If there is no committee, rewrite the sentence
+rather than substituting a plural noun into '`a \{\{CONDUCT_TEAM}}
+member`'.
+
+Appears in:
+
+* `+CODE_OF_CONDUCT.md+`
+
+==== `+{{PGP_KEY_URL}}+`
+
+Public URL the PGP key can be fetched from. Same caveat as
+PGP_FINGERPRINT.
+
+Appears in:
+
+* `+SECURITY.md+`
+
+==== `+{{RESPONSE_TIME}}+`
+
+Initial-response SLA for a security or conduct report. Promise only what
+a solo maintainer can actually meet.
+
+Appears in:
+
+* `+CODE_OF_CONDUCT.md+`
+
+==== `+{{WEBSITE}}+`
+
+Project homepage URL, or delete the field if there is none.
+
+Appears in:
+
+* `+SECURITY.md+`
+
+'''''
+
+Generated by the estate top-up pass. Rationale and the governing rulings
+are in `+hyperpolymath/standards+`; the token vocabulary is
+`+.machine_readable/ai/PLACEHOLDERS.adoc+` in `+rsr-template-repo+`.
diff --git a/REQUIRES_INITIALISATION.md b/REQUIRES_INITIALISATION.md
deleted file mode 100644
index ff1f0a9..0000000
--- a/REQUIRES_INITIALISATION.md
+++ /dev/null
@@ -1,78 +0,0 @@
-
-
-# REQUIRES INITIALISATION
-
-**This repository is not finished being set up.** 4 substitution token(s) across 2 file(s) still have no value.
-
-## Why this is not already done
-
-This repo was created from `hyperpolymath/rsr-template-repo`. The mint
-(`just repo-init`) fills every token that has a single mechanical answer —
-owner, repo, author, dates, licence, branch — and it has done so here.
-
-The tokens below are the ones it *deliberately cannot* answer. They need a
-decision or a fact that exists only in your head: what this project is for,
-what command builds it, which port the service listens on, whether a PGP key
-is held at all. The template's own token vocabulary says as much — you cannot
-sensibly answer "required invariants" in a thirty-second bootstrap.
-
-They were left **visibly unfilled on purpose**. The alternatives were both
-worse: inventing plausible values would put confident falsehoods into a
-security policy and an architecture document, and silently deleting the
-sections would hide the fact that a decision is owed. A visible gap is
-honest; a fabricated answer is not.
-
-## Do not delete this file until every item below is resolved
-
-This file is the only marker that the work is outstanding. Deleting it early
-does not finish the setup, it just conceals it — and the next person or agent
-to arrive will reasonably assume the repo is complete.
-
-- **If you are a person:** delete this file yourself once the last item is done.
-- **If you are an agent:** resolve what you legitimately can, leave the rest,
- and delete this file only when no token below remains anywhere in the tree.
- Do not delete it to make a gate go green.
-
-Re-running the estate top-up tool will remove this file automatically once
-nothing is outstanding, so the safest way to finish is to fix the tokens and
-let the check confirm it.
-
-## What is needed, and where it goes
-
-### `{{CONDUCT_TEAM}}`
-
-Name of the conduct body. If there is no committee, rewrite the sentence rather than substituting a plural noun into 'a {{CONDUCT_TEAM}} member'.
-
-Appears in:
-
-- `CODE_OF_CONDUCT.md`
-
-### `{{PGP_KEY_URL}}`
-
-Public URL the PGP key can be fetched from. Same caveat as PGP_FINGERPRINT.
-
-Appears in:
-
-- `SECURITY.md`
-
-### `{{RESPONSE_TIME}}`
-
-Initial-response SLA for a security or conduct report. Promise only what a solo maintainer can actually meet.
-
-Appears in:
-
-- `CODE_OF_CONDUCT.md`
-
-### `{{WEBSITE}}`
-
-Project homepage URL, or delete the field if there is none.
-
-Appears in:
-
-- `SECURITY.md`
-
----
-
-Generated by the estate top-up pass. Rationale and the governing rulings are
-in `hyperpolymath/standards`; the token vocabulary is
-`.machine_readable/ai/PLACEHOLDERS.adoc` in `rsr-template-repo`.
diff --git a/SECURITY.adoc b/SECURITY.adoc
new file mode 100644
index 0000000..775e783
--- /dev/null
+++ b/SECURITY.adoc
@@ -0,0 +1,452 @@
+== Security Policy
+
+We take security seriously. We appreciate your efforts to responsibly
+disclose vulnerabilities and will make every effort to acknowledge your
+contributions.
+
+=== Table of Contents
+
+* link:#reporting-a-vulnerability[Reporting a Vulnerability]
+* link:#what-to-include[What to Include]
+* link:#response-timeline[Response Timeline]
+* link:#disclosure-policy[Disclosure Policy]
+* link:#scope[Scope]
+* link:#safe-harbour[Safe Harbour]
+* link:#recognition[Recognition]
+* link:#security-updates[Security Updates]
+* link:#security-best-practices[Security Best Practices]
+
+'''''
+
+=== Reporting a Vulnerability
+
+==== Preferred Method: GitHub Security Advisories
+
+The preferred method for reporting security vulnerabilities is through
+GitHub’s Security Advisory feature:
+
+[arabic]
+. Navigate to
+https://github.com/hyperpolymath/nextgen-languages/security/advisories/new[Report
+a Vulnerability]
+. Click *"`Report a vulnerability`"*
+. Complete the form with as much detail as possible
+. Submit — we’ll receive a private notification
+
+This method ensures:
+
+* End-to-end encryption of your report
+* Private discussion space for collaboration
+* Coordinated disclosure tooling
+* Automatic credit when the advisory is published
+
+==== Alternative: Encrypted Email
+
+If you cannot use GitHub Security Advisories, you may email us directly:
+
+[cols=",",]
+|===
+|*Email* |6759885+hyperpolymath@users.noreply.github.com
+|*PGP Key* |link:%7B%7BPGP_KEY_URL%7D%7D[Download Public Key]
+|*Fingerprint* |`+[PGP fingerprint not set]+`
+|===
+
+[source,bash]
+----
+# Import our PGP key
+curl -sSL {{PGP_KEY_URL}} | gpg --import
+
+# Verify fingerprint
+gpg --fingerprint 6759885+hyperpolymath@users.noreply.github.com
+
+# Encrypt your report
+gpg --armor --encrypt --recipient 6759885+hyperpolymath@users.noreply.github.com report.txt
+----
+
+____
+*⚠️ Important:* Do not report security vulnerabilities through public
+GitHub issues, pull requests, discussions, or social media.
+____
+
+'''''
+
+=== What to Include
+
+A good vulnerability report helps us understand and reproduce the issue
+quickly.
+
+==== Required Information
+
+* *Description*: Clear explanation of the vulnerability
+* *Impact*: What an attacker could achieve (confidentiality, integrity,
+availability)
+* *Affected versions*: Which versions/commits are affected
+* *Reproduction steps*: Detailed steps to reproduce the issue
+
+==== Helpful Additional Information
+
+* *Proof of concept*: Code, scripts, or screenshots demonstrating the
+vulnerability
+* *Attack scenario*: Realistic attack scenario showing exploitability
+* *CVSS score*: Your assessment of severity (use
+https://www.first.org/cvss/calculator/3.1[CVSS 3.1 Calculator])
+* *CWE ID*: Common Weakness Enumeration identifier if known
+* *Suggested fix*: If you have ideas for remediation
+* *References*: Links to related vulnerabilities, research, or
+advisories
+
+==== Example Report Structure
+
+[source,markdown]
+----
+## Summary
+[One-sentence description of the vulnerability]
+
+## Vulnerability Type
+[e.g., SQL Injection, XSS, SSRF, Path Traversal, etc.]
+
+## Affected Component
+[File path, function name, API endpoint, etc.]
+
+## Affected Versions
+[Version range or specific commits]
+
+## Severity Assessment
+- CVSS 3.1 Score: [X.X]
+- CVSS Vector: [CVSS:3.1/AV:X/AC:X/PR:X/UI:X/S:X/C:X/I:X/A:X]
+
+## Description
+[Detailed technical description]
+
+## Steps to Reproduce
+1. [First step]
+2. [Second step]
+3. [...]
+
+## Proof of Concept
+[Code, curl commands, screenshots, etc.]
+
+## Impact
+[What can an attacker achieve?]
+
+## Suggested Remediation
+[Optional: your ideas for fixing]
+
+## References
+[Links to related issues, CVEs, research]
+----
+
+'''''
+
+=== Response Timeline
+
+We commit to the following response times:
+
+[width="100%",cols="24%,35%,41%",options="header",]
+|===
+|Stage |Timeframe |Description
+|*Initial Response* |48 hours |We acknowledge receipt and confirm we’re
+investigating
+
+|*Triage* |7 days |We assess severity, confirm the vulnerability, and
+estimate timeline
+
+|*Status Update* |Every 7 days |Regular updates on remediation progress
+
+|*Resolution* |90 days |Target for fix development and release (complex
+issues may take longer)
+
+|*Disclosure* |90 days |Public disclosure after fix is available
+(coordinated with you)
+|===
+
+____
+*Note:* These are targets, not guarantees. Complex vulnerabilities may
+require more time. We’ll communicate openly about any delays.
+____
+
+'''''
+
+=== Disclosure Policy
+
+We follow *coordinated disclosure* (also known as responsible
+disclosure):
+
+[arabic]
+. *You report* the vulnerability privately
+. *We acknowledge* and begin investigation
+. *We develop* a fix and prepare a release
+. *We coordinate* disclosure timing with you
+. *We publish* security advisory and fix simultaneously
+. *You may publish* your research after disclosure
+
+==== Our Commitments
+
+* We will not take legal action against researchers who follow this
+policy
+* We will work with you to understand and resolve the issue
+* We will credit you in the security advisory (unless you prefer
+anonymity)
+* We will notify you before public disclosure
+* We will publish advisories with sufficient detail for users to assess
+risk
+
+==== Your Commitments
+
+* Report vulnerabilities promptly after discovery
+* Give us reasonable time to address the issue before disclosure
+* Do not access, modify, or delete data beyond what’s necessary to
+demonstrate the vulnerability
+* Do not degrade service availability (no DoS testing on production)
+* Do not share vulnerability details with others until coordinated
+disclosure
+
+==== Disclosure Timeline
+
+....
+Day 0 You report vulnerability
+Day 1-2 We acknowledge receipt
+Day 7 We confirm vulnerability and share initial assessment
+Day 7-90 We develop and test fix
+Day 90 Coordinated public disclosure
+ (earlier if fix is ready; later by mutual agreement)
+....
+
+If we cannot reach agreement on disclosure timing, we default to 90 days
+from your initial report.
+
+'''''
+
+=== Scope
+
+==== In Scope ✅
+
+The following are within scope for security research:
+
+* This repository (`+hyperpolymath/nextgen-languages+`) and all its code
+* Official releases and packages published from this repository
+* Documentation that could lead to security issues
+* Build and deployment configurations in this repository
+* Dependencies (report here, we’ll coordinate with upstream)
+
+==== Out of Scope ❌
+
+The following are *not* in scope:
+
+* Third-party services we integrate with (report directly to them)
+* Social engineering attacks against maintainers
+* Physical security
+* Denial of service attacks against production infrastructure
+* Spam, phishing, or other non-technical attacks
+* Issues already reported or publicly known
+* Theoretical vulnerabilities without proof of concept
+
+==== Qualifying Vulnerabilities
+
+We’re particularly interested in:
+
+* Remote code execution
+* SQL injection, command injection, code injection
+* Authentication/authorisation bypass
+* Cross-site scripting (XSS) and cross-site request forgery (CSRF)
+* Server-side request forgery (SSRF)
+* Path traversal / local file inclusion
+* Information disclosure (credentials, PII, secrets)
+* Cryptographic weaknesses
+* Deserialisation vulnerabilities
+* Memory safety issues (buffer overflows, use-after-free, etc.)
+* Supply chain vulnerabilities (dependency confusion, etc.)
+* Significant logic flaws
+
+==== Non-Qualifying Issues
+
+The following generally do not qualify as security vulnerabilities:
+
+* Missing security headers on non-sensitive pages
+* Clickjacking on pages without sensitive actions
+* Self-XSS (requires victim to paste code)
+* Missing rate limiting (unless it enables a specific attack)
+* Username/email enumeration (unless high-risk context)
+* Missing cookie flags on non-sensitive cookies
+* Software version disclosure
+* Verbose error messages (unless exposing secrets)
+* Best practice deviations without demonstrable impact
+
+'''''
+
+=== Safe Harbour
+
+We support security research conducted in good faith.
+
+==== Our Promise
+
+If you conduct security research in accordance with this policy:
+
+* ✅ We will not initiate legal action against you
+* ✅ We will not report your activity to law enforcement
+* ✅ We will work with you in good faith to resolve issues
+* ✅ We consider your research authorised under the Computer Fraud and
+Abuse Act (CFAA), UK Computer Misuse Act, and similar laws
+* ✅ We waive any potential claim against you for circumvention of
+security controls
+
+==== Good Faith Requirements
+
+To qualify for safe harbour, you must:
+
+* Comply with this security policy
+* Report vulnerabilities promptly
+* Avoid privacy violations (do not access others’ data)
+* Avoid service degradation (no destructive testing)
+* Not exploit vulnerabilities beyond proof-of-concept
+* Not use vulnerabilities for profit (beyond bug bounties where offered)
+
+____
+*⚠️ Important:* This safe harbour does not extend to third-party
+systems. Always check their policies before testing.
+____
+
+'''''
+
+=== Recognition
+
+We believe in recognising security researchers who help us improve.
+
+==== Hall of Fame
+
+Researchers who report valid vulnerabilities will be acknowledged in our
+link:SECURITY-ACKNOWLEDGMENTS.md[Security Acknowledgments] (unless they
+prefer anonymity).
+
+Recognition includes:
+
+* Your name (or chosen alias)
+* Link to your website/profile (optional)
+* Brief description of the vulnerability class
+* Date of report
+
+==== What We Offer
+
+* ✅ Public credit in security advisories
+* ✅ Acknowledgment in release notes
+* ✅ Entry in our Hall of Fame
+* ✅ Reference/recommendation letter upon request (for significant
+findings)
+
+==== What We Don’t Currently Offer
+
+* ❌ Monetary bug bounties
+* ❌ Hardware or swag
+* ❌ Paid security research contracts
+
+____
+*Note:* We’re a community project with limited resources. Your
+contributions help everyone who uses this software.
+____
+
+'''''
+
+=== Security Updates
+
+==== Receiving Updates
+
+To stay informed about security updates:
+
+* *Watch this repository*: Click "`Watch`" → "`Custom`" → Select
+"`Security alerts`"
+* *GitHub Security Advisories*: Published at
+https://github.com/hyperpolymath/nextgen-languages/security/advisories[Security
+Advisories]
+* *Release notes*: Security fixes noted in link:CHANGELOG.md[CHANGELOG]
+
+==== Update Policy
+
+[cols=",",options="header",]
+|===
+|Severity |Response
+|*Critical/High* |Patch release as soon as fix is ready
+|*Medium* |Included in next scheduled release (or earlier)
+|*Low* |Included in next scheduled release
+|===
+
+==== Supported Versions
+
+[cols=",,",options="header",]
+|===
+|Version |Supported |Notes
+|`+main+` branch |✅ Yes |Latest development
+|Latest release |✅ Yes |Current stable
+|Previous minor release |✅ Yes |Security fixes backported
+|Older versions |❌ No |Please upgrade
+|===
+
+'''''
+
+=== Security Best Practices
+
+When using Nextgen Languages, we recommend:
+
+==== General
+
+* Keep dependencies up to date
+* Use the latest stable release
+* Subscribe to security notifications
+* Review configuration against security documentation
+* Follow principle of least privilege
+
+==== For Contributors
+
+* Never commit secrets, credentials, or API keys
+* Use signed commits (`+git config commit.gpgsign true+`)
+* Review dependencies before adding them
+* Run security linters locally before pushing
+* Report any concerns about existing code
+
+'''''
+
+=== Additional Resources
+
+* link:%7B%7BPGP_KEY_URL%7D%7D[Our PGP Public Key]
+* https://github.com/hyperpolymath/nextgen-languages/security/advisories[Security
+Advisories]
+* link:CHANGELOG.md[Changelog]
+* link:CONTRIBUTING.md[Contributing Guidelines]
+* https://cve.mitre.org/[CVE Database]
+* https://www.first.org/cvss/calculator/3.1[CVSS Calculator]
+
+'''''
+
+=== Contact
+
+[width="100%",cols="50%,50%",options="header",]
+|===
+|Purpose |Contact
+|*Security issues*
+|https://github.com/hyperpolymath/nextgen-languages/security/advisories/new[Report
+via GitHub] or 6759885+hyperpolymath@users.noreply.github.com
+
+|*General questions*
+|https://github.com/hyperpolymath/nextgen-languages/discussions[GitHub
+Discussions]
+
+|*Other enquiries* |See link:README.md[README] for contact information
+|===
+
+'''''
+
+=== Policy Changes
+
+This security policy may be updated from time to time. Significant
+changes will be:
+
+* Committed to this repository with a clear commit message
+* Noted in the changelog
+* Announced via GitHub Discussions (for major changes)
+
+'''''
+
+_Thank you for helping keep Nextgen Languages and its users safe._ 🛡️
+
+'''''
+
+Last updated: 2026 · Policy version: 1.0.0
diff --git a/SECURITY.md b/SECURITY.md
deleted file mode 100644
index d14783a..0000000
--- a/SECURITY.md
+++ /dev/null
@@ -1,410 +0,0 @@
-
-# Security Policy
-
-
-
-We take security seriously. We appreciate your efforts to responsibly disclose vulnerabilities and will make every effort to acknowledge your contributions.
-
-## Table of Contents
-
-- [Reporting a Vulnerability](#reporting-a-vulnerability)
-- [What to Include](#what-to-include)
-- [Response Timeline](#response-timeline)
-- [Disclosure Policy](#disclosure-policy)
-- [Scope](#scope)
-- [Safe Harbour](#safe-harbour)
-- [Recognition](#recognition)
-- [Security Updates](#security-updates)
-- [Security Best Practices](#security-best-practices)
-
----
-
-## Reporting a Vulnerability
-
-### Preferred Method: GitHub Security Advisories
-
-The preferred method for reporting security vulnerabilities is through GitHub's Security Advisory feature:
-
-1. Navigate to [Report a Vulnerability](https://github.com/hyperpolymath/nextgen-languages/security/advisories/new)
-2. Click **"Report a vulnerability"**
-3. Complete the form with as much detail as possible
-4. Submit — we'll receive a private notification
-
-This method ensures:
-
-- End-to-end encryption of your report
-- Private discussion space for collaboration
-- Coordinated disclosure tooling
-- Automatic credit when the advisory is published
-
-### Alternative: Encrypted Email
-
-If you cannot use GitHub Security Advisories, you may email us directly:
-
-| | |
-|---|---|
-| **Email** | 6759885+hyperpolymath@users.noreply.github.com |
-| **PGP Key** | [Download Public Key]({{PGP_KEY_URL}}) |
-| **Fingerprint** | `[PGP fingerprint not set]` |
-
-```bash
-# Import our PGP key
-curl -sSL {{PGP_KEY_URL}} | gpg --import
-
-# Verify fingerprint
-gpg --fingerprint 6759885+hyperpolymath@users.noreply.github.com
-
-# Encrypt your report
-gpg --armor --encrypt --recipient 6759885+hyperpolymath@users.noreply.github.com report.txt
-```
-
-> **⚠️ Important:** Do not report security vulnerabilities through public GitHub issues, pull requests, discussions, or social media.
-
----
-
-## What to Include
-
-A good vulnerability report helps us understand and reproduce the issue quickly.
-
-### Required Information
-
-- **Description**: Clear explanation of the vulnerability
-- **Impact**: What an attacker could achieve (confidentiality, integrity, availability)
-- **Affected versions**: Which versions/commits are affected
-- **Reproduction steps**: Detailed steps to reproduce the issue
-
-### Helpful Additional Information
-
-- **Proof of concept**: Code, scripts, or screenshots demonstrating the vulnerability
-- **Attack scenario**: Realistic attack scenario showing exploitability
-- **CVSS score**: Your assessment of severity (use [CVSS 3.1 Calculator](https://www.first.org/cvss/calculator/3.1))
-- **CWE ID**: Common Weakness Enumeration identifier if known
-- **Suggested fix**: If you have ideas for remediation
-- **References**: Links to related vulnerabilities, research, or advisories
-
-### Example Report Structure
-
-```markdown
-## Summary
-[One-sentence description of the vulnerability]
-
-## Vulnerability Type
-[e.g., SQL Injection, XSS, SSRF, Path Traversal, etc.]
-
-## Affected Component
-[File path, function name, API endpoint, etc.]
-
-## Affected Versions
-[Version range or specific commits]
-
-## Severity Assessment
-- CVSS 3.1 Score: [X.X]
-- CVSS Vector: [CVSS:3.1/AV:X/AC:X/PR:X/UI:X/S:X/C:X/I:X/A:X]
-
-## Description
-[Detailed technical description]
-
-## Steps to Reproduce
-1. [First step]
-2. [Second step]
-3. [...]
-
-## Proof of Concept
-[Code, curl commands, screenshots, etc.]
-
-## Impact
-[What can an attacker achieve?]
-
-## Suggested Remediation
-[Optional: your ideas for fixing]
-
-## References
-[Links to related issues, CVEs, research]
-```
-
----
-
-## Response Timeline
-
-We commit to the following response times:
-
-| Stage | Timeframe | Description |
-|-------|-----------|-------------|
-| **Initial Response** | 48 hours | We acknowledge receipt and confirm we're investigating |
-| **Triage** | 7 days | We assess severity, confirm the vulnerability, and estimate timeline |
-| **Status Update** | Every 7 days | Regular updates on remediation progress |
-| **Resolution** | 90 days | Target for fix development and release (complex issues may take longer) |
-| **Disclosure** | 90 days | Public disclosure after fix is available (coordinated with you) |
-
-> **Note:** These are targets, not guarantees. Complex vulnerabilities may require more time. We'll communicate openly about any delays.
-
----
-
-## Disclosure Policy
-
-We follow **coordinated disclosure** (also known as responsible disclosure):
-
-1. **You report** the vulnerability privately
-2. **We acknowledge** and begin investigation
-3. **We develop** a fix and prepare a release
-4. **We coordinate** disclosure timing with you
-5. **We publish** security advisory and fix simultaneously
-6. **You may publish** your research after disclosure
-
-### Our Commitments
-
-- We will not take legal action against researchers who follow this policy
-- We will work with you to understand and resolve the issue
-- We will credit you in the security advisory (unless you prefer anonymity)
-- We will notify you before public disclosure
-- We will publish advisories with sufficient detail for users to assess risk
-
-### Your Commitments
-
-- Report vulnerabilities promptly after discovery
-- Give us reasonable time to address the issue before disclosure
-- Do not access, modify, or delete data beyond what's necessary to demonstrate the vulnerability
-- Do not degrade service availability (no DoS testing on production)
-- Do not share vulnerability details with others until coordinated disclosure
-
-### Disclosure Timeline
-
-```
-Day 0 You report vulnerability
-Day 1-2 We acknowledge receipt
-Day 7 We confirm vulnerability and share initial assessment
-Day 7-90 We develop and test fix
-Day 90 Coordinated public disclosure
- (earlier if fix is ready; later by mutual agreement)
-```
-
-If we cannot reach agreement on disclosure timing, we default to 90 days from your initial report.
-
----
-
-## Scope
-
-### In Scope ✅
-
-The following are within scope for security research:
-
-- This repository (`hyperpolymath/nextgen-languages`) and all its code
-- Official releases and packages published from this repository
-- Documentation that could lead to security issues
-- Build and deployment configurations in this repository
-- Dependencies (report here, we'll coordinate with upstream)
-
-### Out of Scope ❌
-
-The following are **not** in scope:
-
-- Third-party services we integrate with (report directly to them)
-- Social engineering attacks against maintainers
-- Physical security
-- Denial of service attacks against production infrastructure
-- Spam, phishing, or other non-technical attacks
-- Issues already reported or publicly known
-- Theoretical vulnerabilities without proof of concept
-
-### Qualifying Vulnerabilities
-
-We're particularly interested in:
-
-- Remote code execution
-- SQL injection, command injection, code injection
-- Authentication/authorisation bypass
-- Cross-site scripting (XSS) and cross-site request forgery (CSRF)
-- Server-side request forgery (SSRF)
-- Path traversal / local file inclusion
-- Information disclosure (credentials, PII, secrets)
-- Cryptographic weaknesses
-- Deserialisation vulnerabilities
-- Memory safety issues (buffer overflows, use-after-free, etc.)
-- Supply chain vulnerabilities (dependency confusion, etc.)
-- Significant logic flaws
-
-### Non-Qualifying Issues
-
-The following generally do not qualify as security vulnerabilities:
-
-- Missing security headers on non-sensitive pages
-- Clickjacking on pages without sensitive actions
-- Self-XSS (requires victim to paste code)
-- Missing rate limiting (unless it enables a specific attack)
-- Username/email enumeration (unless high-risk context)
-- Missing cookie flags on non-sensitive cookies
-- Software version disclosure
-- Verbose error messages (unless exposing secrets)
-- Best practice deviations without demonstrable impact
-
----
-
-## Safe Harbour
-
-We support security research conducted in good faith.
-
-### Our Promise
-
-If you conduct security research in accordance with this policy:
-
-- ✅ We will not initiate legal action against you
-- ✅ We will not report your activity to law enforcement
-- ✅ We will work with you in good faith to resolve issues
-- ✅ We consider your research authorised under the Computer Fraud and Abuse Act (CFAA), UK Computer Misuse Act, and similar laws
-- ✅ We waive any potential claim against you for circumvention of security controls
-
-### Good Faith Requirements
-
-To qualify for safe harbour, you must:
-
-- Comply with this security policy
-- Report vulnerabilities promptly
-- Avoid privacy violations (do not access others' data)
-- Avoid service degradation (no destructive testing)
-- Not exploit vulnerabilities beyond proof-of-concept
-- Not use vulnerabilities for profit (beyond bug bounties where offered)
-
-> **⚠️ Important:** This safe harbour does not extend to third-party systems. Always check their policies before testing.
-
----
-
-## Recognition
-
-We believe in recognising security researchers who help us improve.
-
-### Hall of Fame
-
-Researchers who report valid vulnerabilities will be acknowledged in our [Security Acknowledgments](SECURITY-ACKNOWLEDGMENTS.md) (unless they prefer anonymity).
-
-Recognition includes:
-
-- Your name (or chosen alias)
-- Link to your website/profile (optional)
-- Brief description of the vulnerability class
-- Date of report
-
-### What We Offer
-
-- ✅ Public credit in security advisories
-- ✅ Acknowledgment in release notes
-- ✅ Entry in our Hall of Fame
-- ✅ Reference/recommendation letter upon request (for significant findings)
-
-### What We Don't Currently Offer
-
-- ❌ Monetary bug bounties
-- ❌ Hardware or swag
-- ❌ Paid security research contracts
-
-> **Note:** We're a community project with limited resources. Your contributions help everyone who uses this software.
-
----
-
-## Security Updates
-
-### Receiving Updates
-
-To stay informed about security updates:
-
-- **Watch this repository**: Click "Watch" → "Custom" → Select "Security alerts"
-- **GitHub Security Advisories**: Published at [Security Advisories](https://github.com/hyperpolymath/nextgen-languages/security/advisories)
-- **Release notes**: Security fixes noted in [CHANGELOG](CHANGELOG.md)
-
-### Update Policy
-
-| Severity | Response |
-|----------|----------|
-| **Critical/High** | Patch release as soon as fix is ready |
-| **Medium** | Included in next scheduled release (or earlier) |
-| **Low** | Included in next scheduled release |
-
-### Supported Versions
-
-
-
-| Version | Supported | Notes |
-|---------|-----------|-------|
-| `main` branch | ✅ Yes | Latest development |
-| Latest release | ✅ Yes | Current stable |
-| Previous minor release | ✅ Yes | Security fixes backported |
-| Older versions | ❌ No | Please upgrade |
-
----
-
-## Security Best Practices
-
-When using Nextgen Languages, we recommend:
-
-### General
-
-- Keep dependencies up to date
-- Use the latest stable release
-- Subscribe to security notifications
-- Review configuration against security documentation
-- Follow principle of least privilege
-
-### For Contributors
-
-- Never commit secrets, credentials, or API keys
-- Use signed commits (`git config commit.gpgsign true`)
-- Review dependencies before adding them
-- Run security linters locally before pushing
-- Report any concerns about existing code
-
----
-
-## Additional Resources
-
-- [Our PGP Public Key]({{PGP_KEY_URL}})
-- [Security Advisories](https://github.com/hyperpolymath/nextgen-languages/security/advisories)
-- [Changelog](CHANGELOG.md)
-- [Contributing Guidelines](CONTRIBUTING.md)
-- [CVE Database](https://cve.mitre.org/)
-- [CVSS Calculator](https://www.first.org/cvss/calculator/3.1)
-
----
-
-## Contact
-
-| Purpose | Contact |
-|---------|---------|
-| **Security issues** | [Report via GitHub](https://github.com/hyperpolymath/nextgen-languages/security/advisories/new) or 6759885+hyperpolymath@users.noreply.github.com |
-| **General questions** | [GitHub Discussions](https://github.com/hyperpolymath/nextgen-languages/discussions) |
-| **Other enquiries** | See [README](README.md) for contact information |
-
----
-
-## Policy Changes
-
-This security policy may be updated from time to time. Significant changes will be:
-
-- Committed to this repository with a clear commit message
-- Noted in the changelog
-- Announced via GitHub Discussions (for major changes)
-
----
-
-*Thank you for helping keep Nextgen Languages and its users safe.* 🛡️
-
----
-
-Last updated: 2026 · Policy version: 1.0.0
diff --git a/WHITEPAPER.adoc b/WHITEPAPER.adoc
new file mode 100644
index 0000000..050b790
--- /dev/null
+++ b/WHITEPAPER.adoc
@@ -0,0 +1,478 @@
+== SPDX-License-Identifier: CC-BY-SA-4.0
+
+== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk
+
+== Error-Lang: A Pedagogical Programming Language for Systems Thinking Through Consequence Amplification
+
+*Author:* Jonathan D.A. Jewell *Version:* 1.0 *Date:* 2026-03-14
+*Status:* Production-Ready (v1.0)
+
+'''''
+
+=== Abstract
+
+Error-Lang is a Turing-complete, production-ready programming language
+designed to teach systems thinking by making the consequences of design
+decisions immediately visible and quantifiable. Rather than shielding
+learners from complexity—the dominant approach in pedagogical language
+design since Logo (1967)—Error-Lang employs _consequence amplification_:
+every design choice (mutable state, unchecked nulls, global variables,
+algorithm complexity) produces instant, measurable feedback through a
+real-time _stability score_. The language embodies ten intentional
+design paradoxes that demonstrate _why_ programming languages are
+designed the way they are, transforming error diagnosis from frustrating
+debugging into structured exploration. This paper presents the
+theoretical foundations, the paradox catalogue, the quantum type
+collapse model, and the computational haptics system that together
+constitute a novel pedagogy for programming education.
+
+'''''
+
+=== 1. Introduction
+
+==== 1.1 The Problem with Teaching Programming
+
+Traditional approaches to programming education fall into two camps:
+
+[arabic]
+. *Simplification languages* (Scratch, Logo, BASIC): Hide complexity
+behind abstractions, allowing learners to build working programs without
+understanding why they work. Students struggle to transfer skills to
+production languages because the simplified models are too far from
+reality.
+. *Production languages with training wheels* (Python for beginners,
+JavaScript tutorials): Use real languages but restrict the feature set.
+Students encounter the full language’s complexity without preparation,
+leading to cargo-cult programming—copying patterns without understanding
+their purpose.
+
+Both approaches share a fundamental flaw: they treat errors as obstacles
+rather than learning opportunities. Error messages are designed to be
+"`helpful`" by pointing to solutions, but this bypasses the most
+valuable part of learning— understanding _why_ a constraint exists and
+_what happens_ when it is violated.
+
+==== 1.2 Consequence Amplification
+
+Error-Lang introduces a third approach: *consequence amplification*.
+Instead of preventing mistakes or hiding complexity, Error-Lang makes
+the consequences of every design decision immediately visible:
+
+* Mutable state? The stability score drops by 10 points per mutation.
+* Type instability? −15 per reassignment to a different type.
+* Global state mutation? −30 per occurrence.
+* Unhandled error paths? −25 per failure path.
+* O(n²) algorithm? Penalty proportional to actual execution time.
+
+The key insight is that learners develop _intuition_ for design quality
+when consequences are immediate and quantified, rather than deferred and
+binary (compiles/doesn’t compile, passes tests/doesn’t pass tests).
+
+==== 1.3 Contributions
+
+This paper makes the following contributions:
+
+[arabic]
+. *Consequence amplification* as a pedagogical framework for teaching
+programming (Section 2).
+. *Ten design paradoxes* that embody common language design tradeoffs,
+teaching by contradiction (Section 3).
+. A *quantum type collapse model* that uses physics metaphors to make
+type inference tangible (Section 4).
+. *Computational haptics*: a real-time visual and quantitative feedback
+system for code quality (Section 5).
+. A *five-layer debugging methodology* that reframes error diagnosis as
+structured exploration across compiler phases (Section 6).
+. *Formal verification* of core pedagogical invariants using Idris2
+dependent types (Section 7).
+
+'''''
+
+=== 2. Pedagogical Foundation
+
+==== 2.1 Learning from Consequences vs. Learning from Rules
+
+Kolb’s experiential learning cycle (1984) identifies four stages:
+concrete experience, reflective observation, abstract conceptualisation,
+and active experimentation. Traditional programming education emphasises
+abstract conceptualisation (learn the rules) and active experimentation
+(write code), but underserves concrete experience (see consequences) and
+reflective observation (understand _why_).
+
+Error-Lang’s consequence amplification targets exactly these two
+underserved stages. The stability score provides concrete, quantitative
+experience; the Five Whys and Fishbone analysis tools support reflective
+observation.
+
+==== 2.2 The Stability Score
+
+The stability score is a real-time metric (0–100) that quantifies the
+structural quality of a program:
+
+....
+Stability = Base(100) − Σ(Decision Costs)
+
+Decision Costs:
+ Mutable state: −10 per mutation, −5 per reader
+ Type instability: −15 per type-changing reassignment
+ Null propagation: −20 per unchecked nullable
+ Global state: −30 per mutation
+ Unhandled errors: −25 per failure path
+ Algorithm complexity: −(time_ms / 10)
+ Memory leaks: −10 per KB
+ Race conditions: −40 per conflict
+....
+
+Crucially, the stability score is _not_ a test suite. It is a _live
+metric_ that changes as the student types, providing immediate feedback
+without the delay of running tests. This creates a feedback loop
+analogous to a musician hearing wrong notes immediately rather than
+waiting for an audience review.
+
+==== 2.3 Relationship to Existing Work
+
+Error-Lang’s approach draws on several traditions:
+
+* *Constructionism* (Papert, 1980): Learning through building artefacts,
+but with richer feedback than Logo’s turtle graphics.
+* *Cognitive load theory* (Sweller, 1988): The stability score
+externalises intrinsic complexity, reducing cognitive load by making
+quality visible.
+* *Deliberate practice* (Ericsson, 1993): Immediate feedback on specific
+dimensions of quality supports targeted improvement.
+* *Design patterns as forces* (Alexander, 1977): Each paradox embodies a
+design force; resolution teaches the pattern’s rationale.
+
+'''''
+
+=== 3. The Ten Paradoxes
+
+Error-Lang embodies ten intentional design paradoxes. Each paradox
+violates a principle that students take for granted, forcing them to
+articulate _why_ the principle exists.
+
+==== 3.1 Type Quantum Superposition
+
+*Principle violated:* Variables have a single, deterministic type.
+
+In Error-Lang, untyped variables exist in _superposition_—multiple
+possible types simultaneously—until they are "`observed`" (used in a
+typed context):
+
+[source,error-lang]
+----
+let x = 42 # x is Int|String|Float (superposition)
+print(x + 1) # Collapses to Int: 43
+print(x ++ " hello") # Would collapse to String: "42 hello"
+----
+
+*Pedagogical value:* Students learn that type inference is not magic but
+contextual decision-making. The physics metaphor (wave function
+collapse) makes the abstract concept concrete. The
+nondeterminism—seeded, so reproducible— demonstrates that inference
+_could_ choose differently, highlighting the role of convention and
+language design choices.
+
+==== 3.2 Positional Operator Semantics
+
+*Principle violated:* Operators have fixed semantics regardless of
+position.
+
+[source,error-lang]
+----
+let a = 1 + 2 # Column 12 (even): addition → 3
+let b = 1 + 2 # Column 13 (odd): concatenation → "12"
+----
+
+*Pedagogical value:* Demonstrates that syntax is arbitrary convention.
+Forces students to articulate _why_ consistent semantics matter and
+appreciate that mainstream languages’ consistency is a deliberate design
+choice, not a necessary truth.
+
+==== 3.3 Context-Collapse Keywords
+
+*Principle violated:* Keywords are always keywords; identifiers are
+always identifiers.
+
+At certain nesting depths, keywords become valid identifiers:
+
+[source,error-lang]
+----
+let end = 42 # At depth 1, 'end' is an identifier
+----
+
+*Pedagogical value:* Teaches the distinction between reserved words and
+contextual keywords, and why language designers choose one approach over
+the other.
+
+==== 3.4 Scope Leakage on Primes
+
+*Principle violated:* Lexical scoping is invariant.
+
+Variables leak out of blocks when the run number is prime, the variable
+name is a palindrome, or the declaration line is a Fibonacci number:
+
+[source,error-lang]
+----
+if true
+ let secret = "leaked"
+end
+print(secret) # Error on run #4,6,8 (non-primes)
+ # Works on run #3,5,7,11 (primes!)
+----
+
+*Pedagogical value:* Dramatises the importance of scope rules by showing
+what happens when they are nondeterministic. Makes "`variable lifetime`"
+viscerally real.
+
+==== 3.5 Temporal Corruption
+
+*Principle violated:* Programs are referentially transparent across
+runs.
+
+Previous run history affects current execution via persistent state:
+
+*Pedagogical value:* Demonstrates the dangers of hidden state and why
+functional programming emphasises purity.
+
+==== 3.6–3.10 Additional Paradoxes
+
+The remaining five paradoxes (Reserved Word Roulette, Arithmetic Drift,
+Null Propagation Cascade, Global State Entanglement, Memory Phantom)
+follow the same structure: violate a principle, demonstrate
+consequences, guide the student to articulate the principle’s value.
+Full specifications are in the language’s `+spec/+` directory.
+
+'''''
+
+=== 4. Type System: Quantum Collapse Model
+
+==== 4.1 Formal Definition
+
+The type system models variables as quantum states:
+
+....
+τ ::= Collapsed(T)
+ | Superposition({possibleTypes: [T₁, ..., Tₙ], seed: ℤ, declaredAt: Loc})
+....
+
+*Collapse rules:*
+
+[arabic]
+. _Arithmetic context_: `+x + y+` collapses both operands to `+Int+` or
+`+Float+`.
+. _String context_: `+x ++ y+` collapses to `+String+`.
+. _Comparison context_: `+x > y+` collapses to the "`widest`" numeric
+type.
+. _Print context_: `+print(x)+` collapses to `+String+`.
+. _Type annotation_: `+let x: Int = 42+` prevents superposition
+entirely.
+
+*Determinism guarantee:* Given the same seed and observation context,
+collapse is deterministic. This means programs are reproducible within a
+run but may differ across runs (different seeds), mirroring real physics
+experiments.
+
+==== 4.2 Implementation
+
+The type checker is implemented in AffineScript
+(`+compiler/src/TypeSuperposition.res+`) using algebraic data types for
+quantum states. The seed is derived from the variable’s declaration
+location and the run counter, ensuring reproducibility.
+
+==== 4.3 Relationship to Gradual Typing
+
+Error-Lang’s quantum types share structural similarities with gradual
+typing (Siek & Taha, 2006), but differ in intent:
+
+* *Gradual typing:* Allows mixing typed and untyped code for practical
+flexibility. The dynamic type `+?+` is a convenience.
+* *Quantum types:* Intentionally amplify the consequences of omitting
+type annotations. Superposition is a _pedagogical device_, not a
+practical feature.
+
+'''''
+
+=== 5. Computational Haptics
+
+==== 5.1 Making the Invisible Visible
+
+"`Computational haptics`" is our term for the real-time feedback system
+that makes abstract code quality metrics tangible:
+
+....
+💫 [█████████████░░░░░░░] 65/100
+Stability: FAIR
+
+Factors:
+ Positional semantics: −12
+ Type superposition: −15
+ Mutable state: −8
+ Unhandled errors: −5
+....
+
+The system provides:
+
+* *Animated stability bar* (0–100) with colour coding (green → red).
+* *Per-factor breakdown* showing exactly which decisions cost stability.
+* *Real-time updates* as the student types (via LSP integration).
+* *IDE overlay* highlighting specific lines that reduce stability.
+* *Paradox highlighting* with suggestions for resolution.
+
+==== 5.2 Implementation
+
+The haptics system is implemented in Zig (`+ffi/zig/+`) for performance,
+with AffineScript bindings for the compiler and LSP server. The Zig FFI
+computes stability scores in real-time, including algorithm complexity
+estimation via instruction counting.
+
+'''''
+
+=== 6. Five-Layer Debugging Methodology
+
+==== 6.1 Layers
+
+Error-Lang teaches debugging as _structured exploration_ across five
+compiler/runtime layers:
+
+[cols=",,",options="header",]
+|===
+|Layer |Name |Question
+|1 |Grammar (EBNF) |Is this expression syntactically valid?
+|2 |Parser |How does text become structure?
+|3 |AST |How is code organised?
+|4 |Semantics |What does structure mean?
+|5 |Runtime |What actually happens?
+|===
+
+==== 6.2 Root Cause Analysis Tools
+
+* *Five Whys*: Iterative depth analysis (`+Why → Why → Why → Root+`).
+* *Fishbone Diagram*: Causal categories (Grammar, Parser, Semantics,
+Types, Runtime).
+* *Soft Systems Methodology*: Holistic view of the system.
+
+These tools reframe debugging from "`find and fix the bug`" to
+"`understand the system well enough to explain why the bug exists,`"
+which is a fundamentally different (and more durable) skill.
+
+'''''
+
+=== 7. Formal Verification
+
+==== 7.1 Idris2 Proofs
+
+Error-Lang’s core pedagogical invariants are formally verified using
+Idris2 dependent types:
+
+[arabic]
+. *Stability score determinism*: Given the same source and seed, the
+stability score is the same.
+. *Type collapse determinism*: Given the same seed and context, type
+collapse produces the same type.
+. *Scope leakage correctness*: Leakage occurs if and only if the
+specified conditions hold (primality, palindrome, Fibonacci).
+
+These proofs ensure that the pedagogical properties are
+reliable—students can trust that the language behaves as documented.
+
+==== 7.2 Zig FFI
+
+The formal proofs are bridged to the runtime via a Zig FFI layer
+(`+ffi/zig/+`), following the hyperpolymath Idris2 ABI / Zig FFI
+standard.
+
+'''''
+
+=== 8. Architecture
+
+[width="100%",cols="33%,28%,14%,25%",options="header",]
+|===
+|Component |Language |LOC |Purpose
+|Lexer |AffineScript |605 |Tokenisation with position tracking
+|Parser |AffineScript |952 |CST and AST construction
+|Type Superposition |AffineScript |601 |Quantum type inference engine
+|Stability Tracker |AffineScript |315 |Real-time consequence scoring
+|Analyser |AffineScript |317 |Paradox detection
+|Five Whys Engine |AffineScript |387 |Root cause analysis
+|Layer Navigator |AffineScript |370 |Cross-layer debugging
+|Bytecode VM |AffineScript |520 |Stack-based interpreter
+|Codegen |AffineScript |425 |AST → bytecode compilation
+|LSP Server |AffineScript |310 |IDE integration
+|Computational Haptics |Zig |450 |Real-time feedback engine
+|Formal Proofs |Idris2 |~300 |Pedagogical invariants
+|===
+
+*Total:* ~5,500 LOC (compiler) + ~3,700 LOC (tooling/proofs)
+
+'''''
+
+=== 9. Evaluation
+
+==== 9.1 Target Audience
+
+Error-Lang is designed for:
+
+* *CS education* (introductory and intermediate courses)
+* *Language design courses* (compiler construction, PL theory)
+* *Debugging mastery* (root cause analysis through structured
+exploration)
+* *Code quality awareness* (developing intuition through consequence)
+* *Pedagogical research* (studying learning through intentional
+mistakes)
+
+==== 9.2 Comparison with Existing Pedagogical Languages
+
+[width="100%",cols="20%,12%,18%,12%,14%,24%",options="header",]
+|===
+|Property |Logo |Scratch |Hedy |Pyret |Error-Lang
+|Consequence visibility |None |None |None |Limited |Full (stability
+score)
+
+|Design tradeoff exposure |None |None |None |Some |Intentional (10
+paradoxes)
+
+|Debugging methodology |None |None |None |None |Five Whys + Fishbone
+
+|Real-time feedback |Turtle |Visual |None |None |Computational haptics
+
+|Type system pedagogy |None |None |None |Gradual |Quantum collapse
+
+|Production-capable |No |No |No |Limited |Yes (Turing-complete)
+|===
+
+'''''
+
+=== 10. Conclusion
+
+Error-Lang demonstrates that pedagogical programming languages need not
+choose between simplicity and depth. By making consequences immediate
+and quantifiable, Error-Lang teaches systems thinking without
+sacrificing the ability to build real programs. The ten paradoxes create
+memorable, visceral learning experiences that expose design principles
+students would otherwise accept without examination. The quantum type
+model makes type inference tangible. The stability score externalises
+quality. The Five Whys methodology teaches debugging as exploration.
+
+Together, these innovations suggest a new direction for programming
+education: _teach through consequence, not through rules._
+
+'''''
+
+=== References
+
+[arabic]
+. Alexander, C. (1977). _A Pattern Language_. Oxford University Press.
+. Ericsson, K. A. et al. (1993). "`The Role of Deliberate Practice in
+the Acquisition of Expert Performance.`" _Psychological Review_, 100(3),
+363–406.
+. Kolb, D. A. (1984). _Experiential Learning_. Prentice Hall.
+. Papert, S. (1980). _Mindstorms: Children, Computers, and Powerful
+Ideas_. Basic Books.
+. Pierce, B. C. (2002). _Types and Programming Languages_. MIT Press.
+. Siek, J. G. & Taha, W. (2006). "`Gradual Typing for Functional
+Languages.`" _Scheme and Functional Programming Workshop_, 81–92.
+. Sweller, J. (1988). "`Cognitive Load During Problem Solving: Effects
+on Learning.`" _Cognitive Science_, 12(2), 257–285.
+. Wadler, P. (2015). "`Propositions as Types.`" _Communications of the
+ACM_, 58(12), 75–84.
diff --git a/WHITEPAPER.md b/WHITEPAPER.md
deleted file mode 100644
index 99ab0ea..0000000
--- a/WHITEPAPER.md
+++ /dev/null
@@ -1,435 +0,0 @@
-
-# SPDX-License-Identifier: CC-BY-SA-4.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
-
-# Error-Lang: A Pedagogical Programming Language for Systems Thinking Through Consequence Amplification
-
-**Author:** Jonathan D.A. Jewell
-**Version:** 1.0
-**Date:** 2026-03-14
-**Status:** Production-Ready (v1.0)
-
----
-
-## Abstract
-
-Error-Lang is a Turing-complete, production-ready programming language designed to
-teach systems thinking by making the consequences of design decisions immediately
-visible and quantifiable. Rather than shielding learners from complexity—the
-dominant approach in pedagogical language design since Logo (1967)—Error-Lang
-employs *consequence amplification*: every design choice (mutable state, unchecked
-nulls, global variables, algorithm complexity) produces instant, measurable feedback
-through a real-time *stability score*. The language embodies ten intentional design
-paradoxes that demonstrate *why* programming languages are designed the way they are,
-transforming error diagnosis from frustrating debugging into structured exploration.
-This paper presents the theoretical foundations, the paradox catalogue, the quantum
-type collapse model, and the computational haptics system that together constitute
-a novel pedagogy for programming education.
-
----
-
-## 1. Introduction
-
-### 1.1 The Problem with Teaching Programming
-
-Traditional approaches to programming education fall into two camps:
-
-1. **Simplification languages** (Scratch, Logo, BASIC): Hide complexity behind
- abstractions, allowing learners to build working programs without understanding
- why they work. Students struggle to transfer skills to production languages
- because the simplified models are too far from reality.
-
-2. **Production languages with training wheels** (Python for beginners, JavaScript
- tutorials): Use real languages but restrict the feature set. Students encounter
- the full language's complexity without preparation, leading to cargo-cult
- programming—copying patterns without understanding their purpose.
-
-Both approaches share a fundamental flaw: they treat errors as obstacles rather
-than learning opportunities. Error messages are designed to be "helpful" by
-pointing to solutions, but this bypasses the most valuable part of learning—
-understanding *why* a constraint exists and *what happens* when it is violated.
-
-### 1.2 Consequence Amplification
-
-Error-Lang introduces a third approach: **consequence amplification**. Instead of
-preventing mistakes or hiding complexity, Error-Lang makes the consequences of
-every design decision immediately visible:
-
-- Mutable state? The stability score drops by 10 points per mutation.
-- Type instability? −15 per reassignment to a different type.
-- Global state mutation? −30 per occurrence.
-- Unhandled error paths? −25 per failure path.
-- O(n²) algorithm? Penalty proportional to actual execution time.
-
-The key insight is that learners develop *intuition* for design quality when
-consequences are immediate and quantified, rather than deferred and binary
-(compiles/doesn't compile, passes tests/doesn't pass tests).
-
-### 1.3 Contributions
-
-This paper makes the following contributions:
-
-1. **Consequence amplification** as a pedagogical framework for teaching
- programming (Section 2).
-2. **Ten design paradoxes** that embody common language design tradeoffs,
- teaching by contradiction (Section 3).
-3. A **quantum type collapse model** that uses physics metaphors to make type
- inference tangible (Section 4).
-4. **Computational haptics**: a real-time visual and quantitative feedback
- system for code quality (Section 5).
-5. A **five-layer debugging methodology** that reframes error diagnosis as
- structured exploration across compiler phases (Section 6).
-6. **Formal verification** of core pedagogical invariants using Idris2 dependent
- types (Section 7).
-
----
-
-## 2. Pedagogical Foundation
-
-### 2.1 Learning from Consequences vs. Learning from Rules
-
-Kolb's experiential learning cycle (1984) identifies four stages: concrete
-experience, reflective observation, abstract conceptualisation, and active
-experimentation. Traditional programming education emphasises abstract
-conceptualisation (learn the rules) and active experimentation (write code),
-but underserves concrete experience (see consequences) and reflective observation
-(understand *why*).
-
-Error-Lang's consequence amplification targets exactly these two underserved
-stages. The stability score provides concrete, quantitative experience; the
-Five Whys and Fishbone analysis tools support reflective observation.
-
-### 2.2 The Stability Score
-
-The stability score is a real-time metric (0–100) that quantifies the structural
-quality of a program:
-
-```
-Stability = Base(100) − Σ(Decision Costs)
-
-Decision Costs:
- Mutable state: −10 per mutation, −5 per reader
- Type instability: −15 per type-changing reassignment
- Null propagation: −20 per unchecked nullable
- Global state: −30 per mutation
- Unhandled errors: −25 per failure path
- Algorithm complexity: −(time_ms / 10)
- Memory leaks: −10 per KB
- Race conditions: −40 per conflict
-```
-
-Crucially, the stability score is *not* a test suite. It is a *live metric*
-that changes as the student types, providing immediate feedback without the
-delay of running tests. This creates a feedback loop analogous to a musician
-hearing wrong notes immediately rather than waiting for an audience review.
-
-### 2.3 Relationship to Existing Work
-
-Error-Lang's approach draws on several traditions:
-
-- **Constructionism** (Papert, 1980): Learning through building artefacts, but
- with richer feedback than Logo's turtle graphics.
-- **Cognitive load theory** (Sweller, 1988): The stability score externalises
- intrinsic complexity, reducing cognitive load by making quality visible.
-- **Deliberate practice** (Ericsson, 1993): Immediate feedback on specific
- dimensions of quality supports targeted improvement.
-- **Design patterns as forces** (Alexander, 1977): Each paradox embodies a
- design force; resolution teaches the pattern's rationale.
-
----
-
-## 3. The Ten Paradoxes
-
-Error-Lang embodies ten intentional design paradoxes. Each paradox violates a
-principle that students take for granted, forcing them to articulate *why* the
-principle exists.
-
-### 3.1 Type Quantum Superposition
-
-**Principle violated:** Variables have a single, deterministic type.
-
-In Error-Lang, untyped variables exist in *superposition*—multiple possible types
-simultaneously—until they are "observed" (used in a typed context):
-
-```error-lang
-let x = 42 # x is Int|String|Float (superposition)
-print(x + 1) # Collapses to Int: 43
-print(x ++ " hello") # Would collapse to String: "42 hello"
-```
-
-**Pedagogical value:** Students learn that type inference is not magic but
-contextual decision-making. The physics metaphor (wave function collapse) makes
-the abstract concept concrete. The nondeterminism—seeded, so reproducible—
-demonstrates that inference *could* choose differently, highlighting the role
-of convention and language design choices.
-
-### 3.2 Positional Operator Semantics
-
-**Principle violated:** Operators have fixed semantics regardless of position.
-
-```error-lang
-let a = 1 + 2 # Column 12 (even): addition → 3
-let b = 1 + 2 # Column 13 (odd): concatenation → "12"
-```
-
-**Pedagogical value:** Demonstrates that syntax is arbitrary convention. Forces
-students to articulate *why* consistent semantics matter and appreciate that
-mainstream languages' consistency is a deliberate design choice, not a
-necessary truth.
-
-### 3.3 Context-Collapse Keywords
-
-**Principle violated:** Keywords are always keywords; identifiers are always identifiers.
-
-At certain nesting depths, keywords become valid identifiers:
-
-```error-lang
-let end = 42 # At depth 1, 'end' is an identifier
-```
-
-**Pedagogical value:** Teaches the distinction between reserved words and
-contextual keywords, and why language designers choose one approach over the other.
-
-### 3.4 Scope Leakage on Primes
-
-**Principle violated:** Lexical scoping is invariant.
-
-Variables leak out of blocks when the run number is prime, the variable name
-is a palindrome, or the declaration line is a Fibonacci number:
-
-```error-lang
-if true
- let secret = "leaked"
-end
-print(secret) # Error on run #4,6,8 (non-primes)
- # Works on run #3,5,7,11 (primes!)
-```
-
-**Pedagogical value:** Dramatises the importance of scope rules by showing what
-happens when they are nondeterministic. Makes "variable lifetime" viscerally
-real.
-
-### 3.5 Temporal Corruption
-
-**Principle violated:** Programs are referentially transparent across runs.
-
-Previous run history affects current execution via persistent state:
-
-**Pedagogical value:** Demonstrates the dangers of hidden state and why
-functional programming emphasises purity.
-
-### 3.6–3.10 Additional Paradoxes
-
-The remaining five paradoxes (Reserved Word Roulette, Arithmetic Drift, Null
-Propagation Cascade, Global State Entanglement, Memory Phantom) follow the
-same structure: violate a principle, demonstrate consequences, guide the
-student to articulate the principle's value. Full specifications are in the
-language's `spec/` directory.
-
----
-
-## 4. Type System: Quantum Collapse Model
-
-### 4.1 Formal Definition
-
-The type system models variables as quantum states:
-
-```
-τ ::= Collapsed(T)
- | Superposition({possibleTypes: [T₁, ..., Tₙ], seed: ℤ, declaredAt: Loc})
-```
-
-**Collapse rules:**
-
-1. *Arithmetic context*: `x + y` collapses both operands to `Int` or `Float`.
-2. *String context*: `x ++ y` collapses to `String`.
-3. *Comparison context*: `x > y` collapses to the "widest" numeric type.
-4. *Print context*: `print(x)` collapses to `String`.
-5. *Type annotation*: `let x: Int = 42` prevents superposition entirely.
-
-**Determinism guarantee:** Given the same seed and observation context, collapse
-is deterministic. This means programs are reproducible within a run but may
-differ across runs (different seeds), mirroring real physics experiments.
-
-### 4.2 Implementation
-
-The type checker is implemented in AffineScript (`compiler/src/TypeSuperposition.res`)
-using algebraic data types for quantum states. The seed is derived from the
-variable's declaration location and the run counter, ensuring reproducibility.
-
-### 4.3 Relationship to Gradual Typing
-
-Error-Lang's quantum types share structural similarities with gradual typing
-(Siek & Taha, 2006), but differ in intent:
-
-- **Gradual typing:** Allows mixing typed and untyped code for practical
- flexibility. The dynamic type `?` is a convenience.
-- **Quantum types:** Intentionally amplify the consequences of omitting type
- annotations. Superposition is a *pedagogical device*, not a practical feature.
-
----
-
-## 5. Computational Haptics
-
-### 5.1 Making the Invisible Visible
-
-"Computational haptics" is our term for the real-time feedback system that
-makes abstract code quality metrics tangible:
-
-```
-💫 [█████████████░░░░░░░] 65/100
-Stability: FAIR
-
-Factors:
- Positional semantics: −12
- Type superposition: −15
- Mutable state: −8
- Unhandled errors: −5
-```
-
-The system provides:
-
-- **Animated stability bar** (0–100) with colour coding (green → red).
-- **Per-factor breakdown** showing exactly which decisions cost stability.
-- **Real-time updates** as the student types (via LSP integration).
-- **IDE overlay** highlighting specific lines that reduce stability.
-- **Paradox highlighting** with suggestions for resolution.
-
-### 5.2 Implementation
-
-The haptics system is implemented in Zig (`ffi/zig/`) for performance, with
-AffineScript bindings for the compiler and LSP server. The Zig FFI computes
-stability scores in real-time, including algorithm complexity estimation via
-instruction counting.
-
----
-
-## 6. Five-Layer Debugging Methodology
-
-### 6.1 Layers
-
-Error-Lang teaches debugging as *structured exploration* across five
-compiler/runtime layers:
-
-| Layer | Name | Question |
-|-------|------|----------|
-| 1 | Grammar (EBNF) | Is this expression syntactically valid? |
-| 2 | Parser | How does text become structure? |
-| 3 | AST | How is code organised? |
-| 4 | Semantics | What does structure mean? |
-| 5 | Runtime | What actually happens? |
-
-### 6.2 Root Cause Analysis Tools
-
-- **Five Whys**: Iterative depth analysis (`Why → Why → Why → Root`).
-- **Fishbone Diagram**: Causal categories (Grammar, Parser, Semantics, Types, Runtime).
-- **Soft Systems Methodology**: Holistic view of the system.
-
-These tools reframe debugging from "find and fix the bug" to "understand the
-system well enough to explain why the bug exists," which is a fundamentally
-different (and more durable) skill.
-
----
-
-## 7. Formal Verification
-
-### 7.1 Idris2 Proofs
-
-Error-Lang's core pedagogical invariants are formally verified using Idris2
-dependent types:
-
-1. **Stability score determinism**: Given the same source and seed, the stability
- score is the same.
-2. **Type collapse determinism**: Given the same seed and context, type collapse
- produces the same type.
-3. **Scope leakage correctness**: Leakage occurs if and only if the specified
- conditions hold (primality, palindrome, Fibonacci).
-
-These proofs ensure that the pedagogical properties are reliable—students can
-trust that the language behaves as documented.
-
-### 7.2 Zig FFI
-
-The formal proofs are bridged to the runtime via a Zig FFI layer (`ffi/zig/`),
-following the hyperpolymath Idris2 ABI / Zig FFI standard.
-
----
-
-## 8. Architecture
-
-| Component | Language | LOC | Purpose |
-|-----------|----------|-----|---------|
-| Lexer | AffineScript | 605 | Tokenisation with position tracking |
-| Parser | AffineScript | 952 | CST and AST construction |
-| Type Superposition | AffineScript | 601 | Quantum type inference engine |
-| Stability Tracker | AffineScript | 315 | Real-time consequence scoring |
-| Analyser | AffineScript | 317 | Paradox detection |
-| Five Whys Engine | AffineScript | 387 | Root cause analysis |
-| Layer Navigator | AffineScript | 370 | Cross-layer debugging |
-| Bytecode VM | AffineScript | 520 | Stack-based interpreter |
-| Codegen | AffineScript | 425 | AST → bytecode compilation |
-| LSP Server | AffineScript | 310 | IDE integration |
-| Computational Haptics | Zig | 450 | Real-time feedback engine |
-| Formal Proofs | Idris2 | ~300 | Pedagogical invariants |
-
-**Total:** ~5,500 LOC (compiler) + ~3,700 LOC (tooling/proofs)
-
----
-
-## 9. Evaluation
-
-### 9.1 Target Audience
-
-Error-Lang is designed for:
-
-- **CS education** (introductory and intermediate courses)
-- **Language design courses** (compiler construction, PL theory)
-- **Debugging mastery** (root cause analysis through structured exploration)
-- **Code quality awareness** (developing intuition through consequence)
-- **Pedagogical research** (studying learning through intentional mistakes)
-
-### 9.2 Comparison with Existing Pedagogical Languages
-
-| Property | Logo | Scratch | Hedy | Pyret | Error-Lang |
-|----------|------|---------|------|-------|------------|
-| Consequence visibility | None | None | None | Limited | Full (stability score) |
-| Design tradeoff exposure | None | None | None | Some | Intentional (10 paradoxes) |
-| Debugging methodology | None | None | None | None | Five Whys + Fishbone |
-| Real-time feedback | Turtle | Visual | None | None | Computational haptics |
-| Type system pedagogy | None | None | None | Gradual | Quantum collapse |
-| Production-capable | No | No | No | Limited | Yes (Turing-complete) |
-
----
-
-## 10. Conclusion
-
-Error-Lang demonstrates that pedagogical programming languages need not choose
-between simplicity and depth. By making consequences immediate and quantifiable,
-Error-Lang teaches systems thinking without sacrificing the ability to build real
-programs. The ten paradoxes create memorable, visceral learning experiences that
-expose design principles students would otherwise accept without examination.
-The quantum type model makes type inference tangible. The stability score
-externalises quality. The Five Whys methodology teaches debugging as exploration.
-
-Together, these innovations suggest a new direction for programming education:
-*teach through consequence, not through rules.*
-
----
-
-## References
-
-1. Alexander, C. (1977). *A Pattern Language*. Oxford University Press.
-2. Ericsson, K. A. et al. (1993). "The Role of Deliberate Practice in the
- Acquisition of Expert Performance." *Psychological Review*, 100(3), 363–406.
-3. Kolb, D. A. (1984). *Experiential Learning*. Prentice Hall.
-4. Papert, S. (1980). *Mindstorms: Children, Computers, and Powerful Ideas*. Basic Books.
-5. Pierce, B. C. (2002). *Types and Programming Languages*. MIT Press.
-6. Siek, J. G. & Taha, W. (2006). "Gradual Typing for Functional Languages."
- *Scheme and Functional Programming Workshop*, 81–92.
-7. Sweller, J. (1988). "Cognitive Load During Problem Solving: Effects on
- Learning." *Cognitive Science*, 12(2), 257–285.
-8. Wadler, P. (2015). "Propositions as Types." *Communications of the ACM*,
- 58(12), 75–84.
diff --git a/WOKELANG-COMPARISON.adoc b/WOKELANG-COMPARISON.adoc
new file mode 100644
index 0000000..dd39a8a
--- /dev/null
+++ b/WOKELANG-COMPARISON.adoc
@@ -0,0 +1,207 @@
+== Error-Lang vs WokeLang Feature Comparison
+
+=== Task Summary
+
+*User Request:* Apply the same 4 features implemented for WokeLang to
+Error-Lang.
+
+*The 4 WokeLang Features:* 1. Record field access with dot notation 2.
+Full stdlib integration with interpreter 3. Worker message passing 4.
+Enhanced error messages with hints
+
+=== Error-Lang Current State
+
+*Project Status:* 45% complete (Alpha - Foundation Complete) *Language:*
+Pedagogical language with intentional fragility and paradoxes *Tech
+Stack:* - Compiler: AffineScript - Runtime: Deno (JavaScript) -
+Verification: Idris2 (planned)
+
+==== What Error-Lang Has
+
+*Core Language Features:* - ✅ Lexer, Parser, AST (AffineScript
+compiler) - ✅ Runtime interpreter (Deno/JS) - ✅ Stability tracking
+system (computational haptics) - ✅ 7/10 paradoxes implemented - ✅ Five
+Whys root cause analysis - ✅ Layer navigation (Grammar → AST →
+Semantics → Runtime) - ✅ Visual feedback system (animated stability
+bar)
+
+*AST Support (from Types.res):* - ✅ `+Member(expr, string, location)+`
+- Field access defined - ✅ `+StructDecl+` - Struct declarations defined
+- ✅ `+Struct+` keyword exists - ✅ `+Dot+` operator exists - ✅
+Diagnostics with `+hint: option+` field
+
+=== Feature-by-Feature Analysis
+
+==== Feature 1: Record Field Access ✅ (Partially)
+
+*Status:* AST defined, need to verify runtime implementation
+
+*What’s defined in AST:* - Types.res line 114:
+`+Member(expr, string, location)+` - field access - Types.res line 171:
+`+StructDecl+` - struct declarations - Types.res line 26: `+Struct+`
+keyword - Types.res line 85: `+Dot+` token
+
+*Need to check:* - Is `+Member+` expression evaluated in runtime.js? -
+Can you create struct instances? - Can you access fields with dot
+notation?
+
+*Action required:* Test with example program and implement if missing
+
+'''''
+
+==== Feature 2: Stdlib Integration ❓
+
+*Status:* Need to investigate
+
+Error-Lang appears to have built-in functions (print, println,
+stability()) but no formal stdlib system like WokeLang.
+
+*Evidence:* - Examples use `+println()+`, `+stability()+` - No stdlib
+directory found - No `+Std.*+` module calls in examples
+
+*Questions:* 1. Are there builtin functions beyond print/println? 2. Is
+there a planned stdlib? 3. What functions would make sense for a
+pedagogical language?
+
+*Recommendation:* Error-Lang is a pedagogical language, not
+general-purpose. Stdlib should be *minimal and educational*: - Stability
+tracking functions (already has) - Diagnostic helpers - Basic I/O
+(print/println) - No need for 96 functions like WokeLang
+
+*Action required:* Document existing builtins, add any missing core
+functions
+
+'''''
+
+==== Feature 3: Worker Concurrency ⚠️
+
+*Status:* Not applicable (pedagogical language)
+
+*Reasoning:* Error-Lang is designed to teach systems thinking through
+paradoxes and instability, not general-purpose concurrent programming.
+
+*Language design conflicts:* - Adding workers would introduce
+concurrency complexity - Paradoxes are about sequential execution
+consequences - Stability tracking assumes deterministic execution -
+Educational focus is on cause-and-effect, not parallelism
+
+*Recommendation:* *Do not add workers* - incompatible with pedagogical
+mission
+
+'''''
+
+==== Feature 4: Enhanced Error Messages with Hints ✅ (Partially)
+
+*Status:* Infrastructure exists, needs implementation
+
+*What’s defined:* - Types.res line 196-202: `+diagnostic+` type with
+`+hint: option+` - Types.res line 184-194: Error codes
+E0001-E0010 - Types.res line 282-286: `+formatDiagnostic+` function
+
+*What’s missing:* - Hints not populated (always `+None+` in parser) - No
+suggestion engine - No "`did you mean…?`" for typos - No Levenshtein
+distance matching
+
+*Comparison to Phronesis:* - Phronesis: 967+ lines of comprehensive
+diagnostics - Error-Lang: Basic diagnostic structure, minimal
+implementation
+
+*Action required:* 1. Add hint population to parser error handling 2.
+Create suggestion engine for common mistakes 3. Add educational hints
+for paradox discovery 4. Context-aware error messages
+
+*Educational hints examples:*
+
+....
+Error: Variable 'x' changed type from Int to String
+Hint: This is Type Quantum Superposition! Variables in Error-Lang can exist
+ in multiple types until observed. This teaches how type systems work.
+....
+
+=== Summary
+
+[width="100%",cols="18%,20%,36%,26%",options="header",]
+|===
+|Feature |WokeLang |Error-Lang Status |Work Needed
+|*1. Record field access* |✅ Complete |⚠️ AST defined, runtime unclear
+|Verify + possibly implement
+
+|*2. Stdlib integration* |✅ 96 functions |⚠️ Minimal builtins |Add
+educational builtins
+
+|*3. Worker concurrency* |⚠️ Partial |❌ Not applicable |*None - don’t
+add*
+
+|*4. Enhanced error messages* |⚠️ Design |⚠️ Infrastructure only
+|Implement hints + suggestions
+|===
+
+=== Recommended Work Order
+
+==== Priority 1: Error Messages with Educational Hints
+
+*Why:* Core to pedagogical mission *Work:* 1. Add hint population in
+Parser.res error handling 2. Create paradox-specific error messages 3.
+Add "`what you’re discovering`" explanations 4. Implement suggestion
+engine for typos
+
+==== Priority 2: Verify/Complete Record Field Access
+
+*Why:* Basic language feature *Work:* 1. Test struct creation and field
+access 2. Implement runtime evaluation if missing 3. Add examples
+showing struct usage 4. Document struct syntax
+
+==== Priority 3: Educational Stdlib
+
+*Why:* Enhance teaching capabilities *Work:* 1. Document existing
+builtins (println, stability, etc.) 2. Add diagnostic helpers
+(getDriftMagnitude, getCascadePath) 3. Add educational introspection
+functions 4. Keep minimal - this is not a production language
+
+==== Priority 4: Do NOT Add Workers
+
+*Why:* Incompatible with educational focus *Reasoning:* Error-Lang
+teaches consequence propagation in sequential code, not concurrency
+
+=== Key Differences from WokeLang
+
+*WokeLang:* - General-purpose programming language - Needs full stdlib
+(96 functions) - Workers make sense for concurrent programming - Type
+inference engine with polymorphism
+
+*Error-Lang:* - Pedagogical language with intentional fragility -
+Minimal stdlib (10-15 educational functions) - Workers would obscure
+learning goals - Stability tracking and paradox detection
+
+=== Estimated Work
+
+*Total implementation time:* Much less than WokeLang session
+
+*Breakdown:* - Enhanced error hints: ~2-3 hours (main work) -
+Verify/complete field access: ~1 hour - Educational stdlib: ~1-2 hours -
+Documentation: ~1 hour
+
+*Total:* ~5-7 hours vs. WokeLang’s ~8-10 hours
+
+*Simpler because:* - No complex type inference system to fix - No
+thread-safety concerns - Smaller scope (pedagogical vs general-purpose)
+- AST already has field access defined - Diagnostic infrastructure
+exists
+
+=== Next Steps
+
+[arabic]
+. *Investigate runtime.js* - Check if `+Member+` expression is evaluated
+. *Test struct field access* - Create example program
+. *Implement error hints* - Add educational context to diagnostics
+. *Document builtins* - What functions exist and what they do
+. *Create educational stdlib* - Minimal set of teaching-focused
+functions
+
+=== Files to Create
+
+* `+ERROR-LANG-ANALYSIS.md+` - Detailed implementation plan
+* `+examples/10-struct-fields.err+` - Test struct field access
+* `+docs/Builtins.adoc+` - Document existing functions
+* Updated `+Parser.res+` - Add hint population
+* Updated `+runtime.js+` - Ensure Member evaluation works
diff --git a/WOKELANG-COMPARISON.md b/WOKELANG-COMPARISON.md
deleted file mode 100644
index 6d63c5c..0000000
--- a/WOKELANG-COMPARISON.md
+++ /dev/null
@@ -1,226 +0,0 @@
-
-# Error-Lang vs WokeLang Feature Comparison
-
-## Task Summary
-
-**User Request:** Apply the same 4 features implemented for WokeLang to Error-Lang.
-
-**The 4 WokeLang Features:**
-1. Record field access with dot notation
-2. Full stdlib integration with interpreter
-3. Worker message passing
-4. Enhanced error messages with hints
-
-## Error-Lang Current State
-
-**Project Status:** 45% complete (Alpha - Foundation Complete)
-**Language:** Pedagogical language with intentional fragility and paradoxes
-**Tech Stack:**
-- Compiler: AffineScript
-- Runtime: Deno (JavaScript)
-- Verification: Idris2 (planned)
-
-### What Error-Lang Has
-
-**Core Language Features:**
-- ✅ Lexer, Parser, AST (AffineScript compiler)
-- ✅ Runtime interpreter (Deno/JS)
-- ✅ Stability tracking system (computational haptics)
-- ✅ 7/10 paradoxes implemented
-- ✅ Five Whys root cause analysis
-- ✅ Layer navigation (Grammar → AST → Semantics → Runtime)
-- ✅ Visual feedback system (animated stability bar)
-
-**AST Support (from Types.res):**
-- ✅ `Member(expr, string, location)` - Field access defined
-- ✅ `StructDecl` - Struct declarations defined
-- ✅ `Struct` keyword exists
-- ✅ `Dot` operator exists
-- ✅ Diagnostics with `hint: option` field
-
-## Feature-by-Feature Analysis
-
-### Feature 1: Record Field Access ✅ (Partially)
-
-**Status:** AST defined, need to verify runtime implementation
-
-**What's defined in AST:**
-- Types.res line 114: `Member(expr, string, location)` - field access
-- Types.res line 171: `StructDecl` - struct declarations
-- Types.res line 26: `Struct` keyword
-- Types.res line 85: `Dot` token
-
-**Need to check:**
-- Is `Member` expression evaluated in runtime.js?
-- Can you create struct instances?
-- Can you access fields with dot notation?
-
-**Action required:** Test with example program and implement if missing
-
----
-
-### Feature 2: Stdlib Integration ❓
-
-**Status:** Need to investigate
-
-Error-Lang appears to have built-in functions (print, println, stability()) but no formal stdlib system like WokeLang.
-
-**Evidence:**
-- Examples use `println()`, `stability()`
-- No stdlib directory found
-- No `Std.*` module calls in examples
-
-**Questions:**
-1. Are there builtin functions beyond print/println?
-2. Is there a planned stdlib?
-3. What functions would make sense for a pedagogical language?
-
-**Recommendation:** Error-Lang is a pedagogical language, not general-purpose. Stdlib should be **minimal and educational**:
-- Stability tracking functions (already has)
-- Diagnostic helpers
-- Basic I/O (print/println)
-- No need for 96 functions like WokeLang
-
-**Action required:** Document existing builtins, add any missing core functions
-
----
-
-### Feature 3: Worker Concurrency ⚠️
-
-**Status:** Not applicable (pedagogical language)
-
-**Reasoning:**
-Error-Lang is designed to teach systems thinking through paradoxes and instability, not general-purpose concurrent programming.
-
-**Language design conflicts:**
-- Adding workers would introduce concurrency complexity
-- Paradoxes are about sequential execution consequences
-- Stability tracking assumes deterministic execution
-- Educational focus is on cause-and-effect, not parallelism
-
-**Recommendation:** **Do not add workers** - incompatible with pedagogical mission
-
----
-
-### Feature 4: Enhanced Error Messages with Hints ✅ (Partially)
-
-**Status:** Infrastructure exists, needs implementation
-
-**What's defined:**
-- Types.res line 196-202: `diagnostic` type with `hint: option`
-- Types.res line 184-194: Error codes E0001-E0010
-- Types.res line 282-286: `formatDiagnostic` function
-
-**What's missing:**
-- Hints not populated (always `None` in parser)
-- No suggestion engine
-- No "did you mean...?" for typos
-- No Levenshtein distance matching
-
-**Comparison to Phronesis:**
-- Phronesis: 967+ lines of comprehensive diagnostics
-- Error-Lang: Basic diagnostic structure, minimal implementation
-
-**Action required:**
-1. Add hint population to parser error handling
-2. Create suggestion engine for common mistakes
-3. Add educational hints for paradox discovery
-4. Context-aware error messages
-
-**Educational hints examples:**
-```
-Error: Variable 'x' changed type from Int to String
-Hint: This is Type Quantum Superposition! Variables in Error-Lang can exist
- in multiple types until observed. This teaches how type systems work.
-```
-
-## Summary
-
-| Feature | WokeLang | Error-Lang Status | Work Needed |
-|---------|----------|------------------|-------------|
-| **1. Record field access** | ✅ Complete | ⚠️ AST defined, runtime unclear | Verify + possibly implement |
-| **2. Stdlib integration** | ✅ 96 functions | ⚠️ Minimal builtins | Add educational builtins |
-| **3. Worker concurrency** | ⚠️ Partial | ❌ Not applicable | **None - don't add** |
-| **4. Enhanced error messages** | ⚠️ Design | ⚠️ Infrastructure only | Implement hints + suggestions |
-
-## Recommended Work Order
-
-### Priority 1: Error Messages with Educational Hints
-**Why:** Core to pedagogical mission
-**Work:**
-1. Add hint population in Parser.res error handling
-2. Create paradox-specific error messages
-3. Add "what you're discovering" explanations
-4. Implement suggestion engine for typos
-
-### Priority 2: Verify/Complete Record Field Access
-**Why:** Basic language feature
-**Work:**
-1. Test struct creation and field access
-2. Implement runtime evaluation if missing
-3. Add examples showing struct usage
-4. Document struct syntax
-
-### Priority 3: Educational Stdlib
-**Why:** Enhance teaching capabilities
-**Work:**
-1. Document existing builtins (println, stability, etc.)
-2. Add diagnostic helpers (getDriftMagnitude, getCascadePath)
-3. Add educational introspection functions
-4. Keep minimal - this is not a production language
-
-### Priority 4: Do NOT Add Workers
-**Why:** Incompatible with educational focus
-**Reasoning:** Error-Lang teaches consequence propagation in sequential code, not concurrency
-
-## Key Differences from WokeLang
-
-**WokeLang:**
-- General-purpose programming language
-- Needs full stdlib (96 functions)
-- Workers make sense for concurrent programming
-- Type inference engine with polymorphism
-
-**Error-Lang:**
-- Pedagogical language with intentional fragility
-- Minimal stdlib (10-15 educational functions)
-- Workers would obscure learning goals
-- Stability tracking and paradox detection
-
-## Estimated Work
-
-**Total implementation time:** Much less than WokeLang session
-
-**Breakdown:**
-- Enhanced error hints: ~2-3 hours (main work)
-- Verify/complete field access: ~1 hour
-- Educational stdlib: ~1-2 hours
-- Documentation: ~1 hour
-
-**Total:** ~5-7 hours vs. WokeLang's ~8-10 hours
-
-**Simpler because:**
-- No complex type inference system to fix
-- No thread-safety concerns
-- Smaller scope (pedagogical vs general-purpose)
-- AST already has field access defined
-- Diagnostic infrastructure exists
-
-## Next Steps
-
-1. **Investigate runtime.js** - Check if `Member` expression is evaluated
-2. **Test struct field access** - Create example program
-3. **Implement error hints** - Add educational context to diagnostics
-4. **Document builtins** - What functions exist and what they do
-5. **Create educational stdlib** - Minimal set of teaching-focused functions
-
-## Files to Create
-
-- `ERROR-LANG-ANALYSIS.md` - Detailed implementation plan
-- `examples/10-struct-fields.err` - Test struct field access
-- `docs/Builtins.adoc` - Document existing functions
-- Updated `Parser.res` - Add hint population
-- Updated `runtime.js` - Ensure Member evaluation works
diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc
new file mode 100644
index 0000000..ba74eb4
--- /dev/null
+++ b/docs/tech-debt-2026-05-26.adoc
@@ -0,0 +1,74 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2026
+Jonathan D.A. Jewell (hyperpolymath) –>
+
+== Tech-Debt Audit — error-lang — 2026-05-26
+
+*Source:* estate-wide automated scan 2026-05-26. *Companion:*
+https://github.com/hyperpolymath/standards/tree/main/docs/audits[`+hyperpolymath/standards+`
+2026-05-26-estate-*-debt audits]. *Combined severity:* `+LOW+`.
+
+This file records the _raw findings_ — it does not by itself fix the
+debt. Each section ends with a '`Recommended next move`' line; closing
+the debt is follow-up work.
+
+=== 1. Proof debt
+
+No proof-bearing files (`+*.v+`, `+*.lean+`, `+*.agda+`, `+*.idr+`,
+`+*.idr2+`, `+*.fst+`, `+*.dfy+`, `+*.tla+`, `+*.ads+`, `+*.adb+`) found
+in this repo.
+
+*Recommended next move:* none.
+
+=== 2. Licence debt
+
+[cols=",",options="header",]
+|===
+|Field |Value
+|LICENSE file |`+LICENSE+`
+|SPDX header |`+MPL-2.0+`
+|Manifest licence |`+NONE+`
+|Body classifier |`+Palimp-MPL-2.0+`
+|Severity |`+ok+`
+|===
+
+*Recommended next move:* none for licence.
+
+=== 3. Documentation debt
+
+[cols=",",options="header",]
+|===
+|Field |Value
+|README lines |439
+|`+docs/+` files |7
+|`+docs/+` LoC |2312
+|CHANGELOG.md |N
+|CONTRIBUTING.md |Y
+|CODE_OF_CONDUCT.md |Y
+|SECURITY.md |Y
+|Severity |`+LOW+`
+|===
+
+*Recommended next move:* `+docs/+` has only 7 file(s). Aim for ≥10
+organised docs (architecture, usage, contributing-guide,
+troubleshooting, design-decisions). The user’s bar for a
+"`heavily-developed and well-organised wiki`" is ≥10 files with topical
+organisation.
+
+Additionally: *CHANGELOG.md is missing.* 65% of estate repos lack one —
+adopting a CHANGELOG (or auto-generating via `+git-cliff+`) is a
+recommended estate-wide follow-up.
+
+=== Cross-references
+
+* Estate proof-debt audit:
+`+hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md+`
+* Estate licence-debt audit:
+`+hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md+`
+* Estate documentation-debt audit:
+`+hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md+`
+
+'''''
+
+🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26).
+This file is informational — closing the debt is follow-up work owned by
+the maintainer.
diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md
deleted file mode 100644
index e7ce58c..0000000
--- a/docs/tech-debt-2026-05-26.md
+++ /dev/null
@@ -1,58 +0,0 @@
-
-SPDX-License-Identifier: CC-BY-SA-4.0
-SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
--->
-
-# Tech-Debt Audit — error-lang — 2026-05-26
-
-**Source:** estate-wide automated scan 2026-05-26.
-**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits).
-**Combined severity:** `LOW`.
-
-This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work.
-
-## 1. Proof debt
-
-No proof-bearing files (`*.v`, `*.lean`, `*.agda`, `*.idr`, `*.idr2`, `*.fst`, `*.dfy`, `*.tla`, `*.ads`, `*.adb`) found in this repo.
-
-**Recommended next move:** none.
-
-## 2. Licence debt
-
-| Field | Value |
-|---|---|
-| LICENSE file | `LICENSE` |
-| SPDX header | `MPL-2.0` |
-| Manifest licence | `NONE` |
-| Body classifier | `Palimp-MPL-2.0` |
-| Severity | `ok` |
-
-**Recommended next move:** none for licence.
-
-## 3. Documentation debt
-
-| Field | Value |
-|---|---|
-| README lines | 439 |
-| `docs/` files | 7 |
-| `docs/` LoC | 2312 |
-| CHANGELOG.md | N |
-| CONTRIBUTING.md | Y |
-| CODE_OF_CONDUCT.md | Y |
-| SECURITY.md | Y |
-| Severity | `LOW` |
-
-**Recommended next move:** `docs/` has only 7 file(s). Aim for ≥10 organised docs (architecture, usage, contributing-guide, troubleshooting, design-decisions). The user's bar for a "heavily-developed and well-organised wiki" is ≥10 files with topical organisation.
-
-Additionally: **CHANGELOG.md is missing.** 65% of estate repos lack one — adopting a CHANGELOG (or auto-generating via `git-cliff`) is a recommended estate-wide follow-up.
-
-## Cross-references
-
-- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md`
-- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md`
-- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md`
-
----
-
-🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer.
diff --git a/spec/axiomatic-semantics.md b/spec/axiomatic-semantics.adoc
similarity index 65%
rename from spec/axiomatic-semantics.md
rename to spec/axiomatic-semantics.adoc
index 55942f8..40b32de 100644
--- a/spec/axiomatic-semantics.md
+++ b/spec/axiomatic-semantics.adoc
@@ -1,73 +1,70 @@
-
-# SPDX-License-Identifier: CC-BY-SA-4.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
+== SPDX-License-Identifier: CC-BY-SA-4.0
-# Error-Lang Axiomatic Semantics: Paradox Axioms
+== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk
-**Version:** 1.0.0
-**Date:** 2026-03-14
+== Error-Lang Axiomatic Semantics: Paradox Axioms
----
+*Version:* 1.0.0 *Date:* 2026-03-14
-## 1. Overview
+'''''
-Error-Lang's axiomatic semantics formalise the ten design paradoxes as
+=== 1. Overview
+
+Error-Lang’s axiomatic semantics formalise the ten design paradoxes as
Hoare-style preconditions and postconditions. The key insight is that
-paradoxes are *not* bugs — they are formally specified behaviours with
+paradoxes are _not_ bugs — they are formally specified behaviours with
well-defined pre/postconditions.
-### 1.1 Stability Hoare Triple
+==== 1.1 Stability Hoare Triple
-```
+....
{P, σ} S {Q, σ'}
where σ ∈ [0, 100] is the stability score
-```
+....
-Every statement has a stability impact: `σ' ≤ σ` (stability only decreases).
+Every statement has a stability impact: `+σ' ≤ σ+` (stability only
+decreases).
----
+'''''
-## 2. Paradox 1: Type Quantum Superposition
+=== 2. Paradox 1: Type Quantum Superposition
-### 2.1 Superposition Axiom
+==== 2.1 Superposition Axiom
-```
+....
annotation = None
────────────────────────────────────────────────────────── [P1-Super]
{true, σ} let x = lit {Q(x) = Superposition(…), σ - 15}
(TypeInstability penalty applied)
-```
+....
-### 2.2 Collapse Axiom
+==== 2.2 Collapse Axiom
-```
+....
Q(x) = Superposition(types, seed, loc) context ∈ {Arith, String, …}
hash = (seed + context_hash) mod |types|
τ = types[hash]
────────────────────────────────────────────────────────────── [P1-Collapse]
{Q(x) = Superposition, σ} use(x, context) {Q(x) = Collapsed(τ), σ}
-```
+....
-### 2.3 Annotation Prevention Axiom
+==== 2.3 Annotation Prevention Axiom
-```
+....
────────────────────────────────────────────────────────── [P1-Annotate]
{true, σ} let x: τ = lit {Q(x) = Collapsed(τ), σ}
(no stability penalty)
-```
+....
-**Pedagogical theorem:** Annotations always preserve or improve stability:
-`∀σ. σ_annotated ≥ σ_superposition`.
+*Pedagogical theorem:* Annotations always preserve or improve stability:
+`+∀σ. σ_annotated ≥ σ_superposition+`.
----
+'''''
-## 3. Paradox 2: Positional Operator Semantics
+=== 3. Paradox 2: Positional Operator Semantics
-```
+....
column(op) mod 2 = 0
────────────────────────────────────────────── [P2-Even]
{true, σ} e₁ + e₂ {result = arithmetic(e₁, e₂), σ - 12}
@@ -75,16 +72,16 @@ Every statement has a stability impact: `σ' ≤ σ` (stability only decreases).
column(op) mod 2 = 1
────────────────────────────────────────────── [P2-Odd]
{true, σ} e₁ + e₂ {result = concat(toString(e₁), toString(e₂)), σ - 12}
-```
+....
-**Axiom (determinism):** For a fixed source position, the operator semantics
-are deterministic. Reformatting the code may change behaviour.
+*Axiom (determinism):* For a fixed source position, the operator
+semantics are deterministic. Reformatting the code may change behaviour.
----
+'''''
-## 4. Paradox 3: Context-Collapse Keywords
+=== 4. Paradox 3: Context-Collapse Keywords
-```
+....
depth ≥ 1
──────────────────────────────────────────── [P3-Collapse]
{nesting_depth = depth, σ} let end = e {end ∈ dom(ρ), σ}
@@ -94,13 +91,13 @@ are deterministic. Reformatting the code may change behaviour.
──────────────────────────────────────────── [P3-Reserved]
{nesting_depth = 0, σ} let end = e {⊥}
(parse error: keyword used as identifier)
-```
+....
----
+'''''
-## 5. Paradox 4: Scope Leakage on Primes
+=== 5. Paradox 4: Scope Leakage on Primes
-```
+....
is_prime(run_counter) ∨ is_palindrome(x) ∨ is_fibonacci(line)
──────────────────────────────────────────────────────────────── [P4-Leak]
{true, σ} { let x = v; } {x ∈ dom(ρ_parent), σ}
@@ -110,16 +107,16 @@ are deterministic. Reformatting the code may change behaviour.
────────────────────────────────────────────────────────────────── [P4-Normal]
{true, σ} { let x = v; } {x ∉ dom(ρ_parent), σ}
(standard lexical scoping)
-```
+....
-**Axiom (leakage determinism):** Leakage is a pure function of
-`(run_counter, variable_name, line_number)`.
+*Axiom (leakage determinism):* Leakage is a pure function of
+`+(run_counter, variable_name, line_number)+`.
----
+'''''
-## 6. Paradox 5: Temporal Corruption
+=== 6. Paradox 5: Temporal Corruption
-```
+....
temporal_history ≠ [] value affected by history
────────────────────────────────────────────────── [P5-Corrupt]
{temporal_history = H, σ} eval(e) {result depends on H, σ}
@@ -127,71 +124,74 @@ are deterministic. Reformatting the code may change behaviour.
temporal_history = [] (first run)
────────────────────────────────────────────── [P5-Clean]
{temporal_history = [], σ} eval(e) {result independent of H, σ}
-```
+....
----
+'''''
-## 7. Stability Axioms
+=== 7. Stability Axioms
-### 7.1 Stability Monotonicity
+==== 7.1 Stability Monotonicity
-```
+....
{P, σ} S {Q, σ'}
────────────────── [Stab-Mono]
σ' ≤ σ (stability never increases)
-```
+....
-### 7.2 Stability Penalty Accumulation
+==== 7.2 Stability Penalty Accumulation
-```
+....
{P, σ} S₁ {Q, σ₁} {Q, σ₁} S₂ {T, σ₂}
───────────────────────────────────────────── [Stab-Seq]
{P, σ} S₁; S₂ {T, σ₂}
where σ₂ = σ - penalty(S₁) - penalty(S₂)
-```
+....
-### 7.3 Stability Floor
+==== 7.3 Stability Floor
-```
+....
σ - penalty(S) < 0
────────────────────── [Stab-Floor]
σ' = 0 (stability clamped to 0, never negative)
-```
+....
----
+'''''
-## 8. Gutter Block Axioms
+=== 8. Gutter Block Axioms
-```
+....
body contains parse errors
──────────────────────────────────────────────── [Gutter-Recovery]
{true, σ} gutter { body } end {errors collected, σ}
(parser always recovers; no crash; errors available for inspection)
-```
+....
-**Safety axiom:** A gutter block never causes program termination.
+*Safety axiom:* A gutter block never causes program termination.
----
+'''''
-## 9. Key Theorems
+=== 9. Key Theorems
-### 9.1 Annotation Optimality
+==== 9.1 Annotation Optimality
-**Theorem:** For any program P, the variant P' with all type annotations added
-has stability(P') ≥ stability(P). Type annotations are always beneficial.
+*Theorem:* For any program P, the variant P’ with all type annotations
+added has stability(P’) ≥ stability(P). Type annotations are always
+beneficial.
-### 9.2 Paradox Determinism
+==== 9.2 Paradox Determinism
-**Theorem:** All ten paradoxes are deterministic given the same
-`(source, run_counter, seed)` triple. Non-determinism is apparent, not actual.
+*Theorem:* All ten paradoxes are deterministic given the same
+`+(source, run_counter, seed)+` triple. Non-determinism is apparent, not
+actual.
-### 9.3 Stability as Loop Variant
+==== 9.3 Stability as Loop Variant
-**Theorem:** If every loop body consumes at least δ > 0 stability, then all
-loops terminate within ⌈100/δ⌉ iterations (since stability starts at 100 and
-is bounded below by 0).
+*Theorem:* If every loop body consumes at least δ > 0 stability, then
+all loops terminate within ⌈100/δ⌉ iterations (since stability starts at
+100 and is bounded below by 0).
-### 9.4 Pedagogical Completeness
+==== 9.4 Pedagogical Completeness
-**Theorem:** Every violation of a "standard" programming principle corresponds
-to a measurable stability penalty, ensuring no design tradeoff is invisible.
+*Theorem:* Every violation of a "`standard`" programming principle
+corresponds to a measurable stability penalty, ensuring no design
+tradeoff is invisible.
diff --git a/spec/operational-semantics.md b/spec/operational-semantics.adoc
similarity index 83%
rename from spec/operational-semantics.md
rename to spec/operational-semantics.adoc
index 57c7316..61adce3 100644
--- a/spec/operational-semantics.md
+++ b/spec/operational-semantics.adoc
@@ -1,29 +1,27 @@
-
-# SPDX-License-Identifier: CC-BY-SA-4.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
+== SPDX-License-Identifier: CC-BY-SA-4.0
-# Error-Lang Operational Semantics
+== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk
-**Version:** 1.0.0
-**Date:** 2026-03-14
+== Error-Lang Operational Semantics
----
+*Version:* 1.0.0 *Date:* 2026-03-14
-## 1. Notation
+'''''
-- `ρ` — Environment (variable bindings)
-- `Σ` — Interpreter state (stability score, run counter, paradox state)
-- `ρ, Σ ⊢ e ⇓ v, Σ'` — Expression `e` evaluates to value `v` with updated state
-- `⊥` — Error
+=== 1. Notation
----
+* `+ρ+` — Environment (variable bindings)
+* `+Σ+` — Interpreter state (stability score, run counter, paradox
+state)
+* `+ρ, Σ ⊢ e ⇓ v, Σ'+` — Expression `+e+` evaluates to value `+v+` with
+updated state
+* `+⊥+` — Error
-## 2. Values
+'''''
-```
+=== 2. Values
+
+....
v ∈ Value ::=
() unit
| b ∈ {true, false} boolean
@@ -34,13 +32,13 @@ v ∈ Value ::=
| Fn(name, params, body, ρ_closure) function closure
| Builtin(name, impl) built-in function
| Quantum(possible_types, seed, loc) type in superposition
-```
+....
----
+'''''
-## 3. Interpreter State
+=== 3. Interpreter State
-```
+....
Σ = ⟨ stability : ℝ ∈ [0, 100] (initially 100),
run_counter : ℕ (persistent across runs),
paradox_state : ParadoxState,
@@ -52,15 +50,15 @@ ParadoxState = ⟨
scope_leaks : Set, Paradox 4: leaked variables
temporal_history : List Paradox 5: previous run state
⟩
-```
+....
----
+'''''
-## 4. Stability Score
+=== 4. Stability Score
The stability score is a real-time metric updated by a penalty function:
-```
+....
penalty : Decision → ℝ
penalty(MutableState) = 10
penalty(MutableReader) = 5
@@ -73,24 +71,24 @@ penalty(MemoryLeak(kb)) = kb × 10
penalty(RaceCondition) = 40
apply_penalty(Σ, d) = Σ[stability ↦ max(0, Σ.stability − penalty(d))]
-```
+....
----
+'''''
-## 5. Quantum Type Collapse (Paradox 1)
+=== 5. Quantum Type Collapse (Paradox 1)
-### 5.1 Superposition Creation
+==== 5.1 Superposition Creation
-```
+....
no type annotation on x seed = hash(loc, Σ.run_counter)
───────────────────────────────────────────────────────────── [Super-Create]
ρ, Σ ⊢ let x = 42 ⇒ ρ[x ↦ Quantum([Int, Float, String], seed, loc)], Σ'
where Σ' = apply_penalty(Σ, TypeInstability)
-```
+....
-### 5.2 Collapse Rules
+==== 5.2 Collapse Rules
-```
+....
ρ(x) = Quantum(types, seed, loc) context = Arithmetic
collapsed = deterministic_select(types ∩ Numeric, seed)
─────────────────────────────────────────────────────── [Collapse-Arith]
@@ -103,21 +101,21 @@ apply_penalty(Σ, d) = Σ[stability ↦ max(0, Σ.stability − penalty(d))]
ρ(x) = Quantum(types, seed, loc) context = Print
────────────────────────────────────────────────────── [Collapse-Print]
ρ, Σ ⊢ println(x) ⇓ println(toString(ρ(x)))
-```
+....
-### 5.3 Annotation Prevents Superposition
+==== 5.3 Annotation Prevents Superposition
-```
+....
type annotation present
────────────────────────────────────────────── [No-Super]
ρ, Σ ⊢ let x: Int = 42 ⇒ ρ[x ↦ 42], Σ (no penalty)
-```
+....
----
+'''''
-## 6. Positional Operator Semantics (Paradox 2)
+=== 6. Positional Operator Semantics (Paradox 2)
-```
+....
column(+) = c c mod 2 = 0
ρ, Σ ⊢ e₁ ⇓ v₁ ρ, Σ ⊢ e₂ ⇓ v₂
────────────────────────────────────── [Pos-Add]
@@ -129,13 +127,13 @@ apply_penalty(Σ, d) = Σ[stability ↦ max(0, Σ.stability − penalty(d))]
ρ, Σ ⊢ e₁ + e₂ ⇓ toString(v₁) ++ toString(v₂) (string concatenation)
Σ' = apply_penalty(Σ, PositionalSemantics)
-```
+....
----
+'''''
-## 7. Context-Collapse Keywords (Paradox 3)
+=== 7. Context-Collapse Keywords (Paradox 3)
-```
+....
Σ.paradox_state.context_depth = d d ≥ 1 "end" used as identifier
───────────────────────────────────────────────────────────────────────── [Ctx-Collapse]
ρ, Σ ⊢ let end = 42 ⇒ ρ[end ↦ 42], Σ (keyword becomes identifier)
@@ -143,13 +141,13 @@ apply_penalty(Σ, d) = Σ[stability ↦ max(0, Σ.stability − penalty(d))]
Σ.paradox_state.context_depth = 0 "end" used as identifier
─────────────────────────────────────────────────────────────────── [Ctx-Reserved]
ρ, Σ ⊢ let end = 42 ⇓ ⊥("unexpected keyword 'end'")
-```
+....
----
+'''''
-## 8. Scope Leakage (Paradox 4)
+=== 8. Scope Leakage (Paradox 4)
-```
+....
is_prime(Σ.run_counter) = true
∨ is_palindrome(x) = true
∨ is_fibonacci(line_number) = true
@@ -161,25 +159,25 @@ apply_penalty(Σ, d) = Σ[stability ↦ max(0, Σ.stability − penalty(d))]
∧ is_fibonacci(line_number) = false
───────────────────────────────────────────── [Scope-Normal]
Variable x follows standard lexical scoping (does not leak)
-```
+....
----
+'''''
-## 9. Standard Expression Evaluation
+=== 9. Standard Expression Evaluation
-### 9.1 Literals
+==== 9.1 Literals
-```
+....
────────────── [Lit-Int] ────────────── [Lit-Float]
ρ, Σ ⊢ n ⇓ n ρ, Σ ⊢ f ⇓ f
────────────── [Lit-String] ────────────── [Lit-Bool]
ρ, Σ ⊢ s ⇓ s ρ, Σ ⊢ b ⇓ b
-```
+....
-### 9.2 Variables
+==== 9.2 Variables
-```
+....
x ∈ dom(ρ) ∪ Σ.paradox_state.scope_leaks
────────────────────────────────────────── [Var]
ρ, Σ ⊢ x ⇓ ρ(x)
@@ -187,11 +185,11 @@ apply_penalty(Σ, d) = Σ[stability ↦ max(0, Σ.stability − penalty(d))]
x ∉ dom(ρ) ∧ x ∉ Σ.paradox_state.scope_leaks
─────────────────────────────────────────────── [Var-Undef]
ρ, Σ ⊢ x ⇓ ⊥("undefined variable: " ++ x)
-```
+....
-### 9.3 Binary Operations (non-positional)
+==== 9.3 Binary Operations (non-positional)
-```
+....
ρ, Σ ⊢ e₁ ⇓ v₁ ρ, Σ ⊢ e₂ ⇓ v₂ v₁, v₂ numeric
───────────────────────────────────────────────────────── [Arith]
ρ, Σ ⊢ e₁ ⊕ e₂ ⇓ v₁ ⊕ v₂ for ⊕ ∈ {+, -, *, /, %}
@@ -207,11 +205,11 @@ apply_penalty(Σ, d) = Σ[stability ↦ max(0, Σ.stability − penalty(d))]
ρ, Σ ⊢ e₁ ⇓ v₁ truthy(v₁) = true
────────────────────────────────────────── [Or-Short]
ρ, Σ ⊢ e₁ or e₂ ⇓ true
-```
+....
-### 9.4 Unary
+==== 9.4 Unary
-```
+....
ρ, Σ ⊢ e ⇓ v v numeric
────────────────────────── [Neg]
ρ, Σ ⊢ -e ⇓ -v
@@ -219,35 +217,35 @@ apply_penalty(Σ, d) = Σ[stability ↦ max(0, Σ.stability − penalty(d))]
ρ, Σ ⊢ e ⇓ v
────────────────────────── [Not]
ρ, Σ ⊢ not e ⇓ ¬truthy(v)
-```
+....
----
+'''''
-## 10. Statements
+=== 10. Statements
-### 10.1 Let (with stability tracking)
+==== 10.1 Let (with stability tracking)
-```
+....
ρ, Σ ⊢ e ⇓ v
ρ' = ρ[x ↦ v]
Σ' = if mutable then apply_penalty(Σ, MutableState) else Σ
───────────────────────────────────────────────────────── [Let]
ρ, Σ ⊢ let [mutable] x = e ⇒ ρ', Σ'
-```
+....
-### 10.2 Assignment (stability penalty)
+==== 10.2 Assignment (stability penalty)
-```
+....
x ∈ dom(ρ) ρ, Σ ⊢ e ⇓ v
Σ' = apply_penalty(Σ, MutableState)
type(ρ(x)) ≠ type(v) ⟹ Σ'' = apply_penalty(Σ', TypeInstability)
───────────────────────────────────────────────────────── [Assign]
ρ, Σ ⊢ x = e ⇒ ρ[x ↦ v], Σ''
-```
+....
-### 10.3 Control Flow
+==== 10.3 Control Flow
-```
+....
ρ, Σ ⊢ cond ⇓ v truthy(v) = true ρ, Σ ⊢ then ⇒ ρ', Σ'
─────────────────────────────────────────────────────────────────── [If-True]
ρ, Σ ⊢ if cond { then } [else { els }] ⇒ ρ', Σ'
@@ -264,43 +262,43 @@ apply_penalty(Σ, d) = Σ[stability ↦ max(0, Σ.stability − penalty(d))]
ρ, Σ ⊢ cond ⇓ v truthy(v) = false
────────────────────────────────────────── [While-Done]
ρ, Σ ⊢ while cond { body } ⇒ ρ, Σ
-```
+....
-### 10.4 Return
+==== 10.4 Return
-```
+....
ρ, Σ ⊢ e ⇓ v
────────────────────────────────── [Return]
ρ, Σ ⊢ return e ⇒ raise Return(v)
-```
+....
-### 10.5 Gutter Block (Error Injection Zone)
+==== 10.5 Gutter Block (Error Injection Zone)
-```
+....
parse(body) = errors errors recovered
──────────────────────────────────────────── [Gutter]
ρ, Σ ⊢ gutter { body } end ⇒ ρ, Σ
(parser recovers; errors collected for pedagogical display)
-```
+....
----
+'''''
-## 11. Function Calls
+=== 11. Function Calls
-```
+....
ρ, Σ ⊢ f ⇓ Fn(name, [p₁,…,pₙ], body, ρ_clos)
∀i. ρ, Σ ⊢ aᵢ ⇓ vᵢ m = n
ρ_call = ρ_clos[p₁ ↦ v₁, …, pₙ ↦ vₙ]
ρ_call, Σ ⊢ body ⇓ v' (catch Return(v') → v')
──────────────────────────────────────────────────── [Call]
ρ, Σ ⊢ f(a₁, …, aₘ) ⇓ v'
-```
+....
----
+'''''
-## 12. Pattern Matching
+=== 12. Pattern Matching
-```
+....
ρ, Σ ⊢ scrutinee ⇓ v
∃i: match(armᵢ.pat, v) = binds
ρ ∪ binds, Σ ⊢ armᵢ.body ⇓ v'
@@ -310,38 +308,39 @@ apply_penalty(Σ, d) = Σ[stability ↦ max(0, Σ.stability − penalty(d))]
match(_, v) = {} [Wild]
match(x, v) = {x ↦ v} [Var]
match(lit, v) = {} if lit = v [Lit]
-```
+....
----
+'''''
-## 13. Stability Query
+=== 13. Stability Query
-```
+....
────────────────────────────────────── [Stability]
ρ, Σ ⊢ stability() ⇓ Σ.stability
-```
+....
----
+'''''
-## 14. Five-Layer Navigation
+=== 14. Five-Layer Navigation
-The interpreter tracks which layer (Grammar, Parser, AST, Semantics, Runtime)
-an error originates from. Each error carries a `layer : Layer` tag:
+The interpreter tracks which layer (Grammar, Parser, AST, Semantics,
+Runtime) an error originates from. Each error carries a
+`+layer : Layer+` tag:
-```
+....
Layer ::= Grammar | Parser | AST | Semantics | Runtime
error_with_layer(msg, layer) = Error(msg, layer, line, column)
-```
+....
This enables the Five Whys debugging methodology: tracing from Runtime
down through Semantics → AST → Parser → Grammar.
----
+'''''
-## 15. Program Execution
+=== 15. Program Execution
-```
+....
ρ₀ = ∅ register_builtins(ρ₀)
Σ₀ = ⟨100, load_run_counter(), fresh_paradox_state(), seed⟩
∀item: register(item, ρ₀)
@@ -349,18 +348,26 @@ down through Semantics → AST → Parser → Grammar.
save_run_counter(Σ_final.run_counter + 1)
────────────────────────────────────────────── [Program]
run(file) ⇓ (v, Σ_final.stability)
-```
-
-The run counter is persisted to `~/.config/error-lang/run_counter`,
-enabling Paradox 4 (scope leakage on primes) and Paradox 5 (temporal corruption).
-
----
-
-## 16. Invariants
-
-1. **Stability monotonically decreasing:** Penalties only subtract; no operation increases stability.
-2. **Type collapse determinism:** Given same seed and context, collapse produces the same type.
-3. **Scope leak determinism:** Leakage is a pure function of run_counter, variable name, and line number.
-4. **Positional determinism:** Operator semantics are a pure function of source column.
-5. **Run counter persistence:** Counter survives across process invocations.
-6. **Gutter recovery:** Parser always recovers from gutter block errors; they never crash the program.
+....
+
+The run counter is persisted to `+~/.config/error-lang/run_counter+`,
+enabling Paradox 4 (scope leakage on primes) and Paradox 5 (temporal
+corruption).
+
+'''''
+
+=== 16. Invariants
+
+[arabic]
+. *Stability monotonically decreasing:* Penalties only subtract; no
+operation increases stability.
+. *Type collapse determinism:* Given same seed and context, collapse
+produces the same type.
+. *Scope leak determinism:* Leakage is a pure function of run_counter,
+variable name, and line number.
+. *Positional determinism:* Operator semantics are a pure function of
+source column.
+. *Run counter persistence:* Counter survives across process
+invocations.
+. *Gutter recovery:* Parser always recovers from gutter block errors;
+they never crash the program.
diff --git a/spec/system-specs.adoc b/spec/system-specs.adoc
new file mode 100644
index 0000000..ca5ffc7
--- /dev/null
+++ b/spec/system-specs.adoc
@@ -0,0 +1,183 @@
+== SPDX-License-Identifier: CC-BY-SA-4.0
+
+== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk
+
+== Error-Lang System Specifications
+
+Error-Lang is a pedagogical programming language where errors are
+features. Implementation stack: AffineScript compiler (compiles to
+JavaScript), Zig FFI for computational haptics feedback. Designed for
+learning through deliberate failure.
+
+'''''
+
+=== Memory Model
+
+Error-Lang’s memory model is intentionally simple, befitting its
+pedagogical purpose, with a specialised FFI layer for haptics.
+
+==== JavaScript Runtime (Primary)
+
+* AffineScript compiles to JavaScript; all Error-Lang values are JS heap
+objects managed by the JavaScript engine’s garbage collector.
+* No manual memory management is exposed to Error-Lang users.
+* Values are immutable by default (AffineScript’s functional core).
+* Mutable state is limited to the interpreter’s internal bookkeeping.
+
+==== Interpreter State
+
+* The interpreter maintains a `+StabilityState+` struct containing:
+** *stability_score*: `+float+` — current program stability (0.0 to
+1.0).
+** *paradox_level*: `+int+` — depth of active paradox nesting.
+** *error_history*: `+array+` — log of all errors
+encountered.
+** *correction_attempts*: `+int+` — number of user fix attempts this
+session.
+* This state persists across statements within a single REPL session or
+file execution and is reset between sessions.
+
+==== Zig FFI Layer (Computational Haptics)
+
+* The Zig FFI module manages its own memory via `+std.mem.Allocator+`.
+* Haptic feedback buffers are allocated per-event and freed after
+transmission to the haptic device.
+* No GC interaction — Zig allocations are invisible to the JS runtime.
+* Data crossing the FFI boundary is serialised to C-compatible structs
+defined in `+generated/abi/haptics.h+`.
+
+==== Memory Invariants
+
+* Error-Lang programs cannot cause memory leaks in user-space (GC
+handles all).
+* Zig FFI allocations are bounded: at most one haptic buffer active at a
+time.
+* The stability state struct has a fixed, small memory footprint.
+
+'''''
+
+=== Concurrency Model
+
+Error-Lang is deliberately single-threaded.
+
+==== Design Rationale
+
+* Concurrency adds complexity that conflicts with pedagogical goals.
+* Learners should focus on understanding errors and stability, not race
+conditions or deadlocks.
+* The single-threaded model makes program behaviour fully deterministic
+(modulo stability score thresholds).
+
+==== Execution Model
+
+* Statements execute sequentially in source order.
+* The REPL processes one input at a time, updating stability state after
+each.
+* No async operations, no event loop, no callbacks.
+
+==== Haptic Feedback Timing
+
+* Zig FFI calls for haptic feedback are synchronous and blocking.
+* Haptic events are brief (< 50ms) so blocking is imperceptible.
+* If no haptic device is connected, the FFI call returns immediately
+(no-op).
+
+'''''
+
+=== Effect System
+
+Error-Lang’s effect system is unconventional: stability impact and
+paradox state are the primary tracked effects.
+
+==== Stability as Effect
+
+Every statement in Error-Lang has a stability impact:
+
+[width="99%",cols="27%,32%,41%",options="header",]
+|===
+|Category |Stability Effect |Example
+|Correct statement |`++0.05+` to `++0.10+` |Valid assignment, correct
+logic
+
+|Syntax error |`+-0.15+` to `+-0.25+` |Missing semicolon, bad indent
+
+|Type error |`+-0.10+` to `+-0.20+` |Wrong argument type
+
+|Deliberate error |`++0.02+` (learning bonus) |Annotated with
+`+@intentional+`
+
+|Error correction |`++0.15+` to `++0.20+` |Fixing a previous error
+
+|Repeated error |`+-0.30+` (penalty) |Same error class within 5 stmts
+|===
+
+* Stability is checked implicitly after every statement.
+* When stability drops below `+0.2+`, the interpreter enters "`crisis
+mode`" — haptic feedback intensifies and hints become more explicit.
+* When stability reaches `+1.0+`, the session is "`mastered.`"
+
+==== Paradox State as Implicit Effect
+
+* Certain constructs create paradoxes (self-referential errors,
+contradictions).
+* Paradox depth is tracked as an implicit effect counter.
+* Paradoxes cannot be nested beyond depth 3 (interpreter rejects deeper
+nesting).
+* Resolving a paradox grants a significant stability bonus (`++0.25+`).
+
+==== Haptic Effect
+
+* Error events trigger haptic feedback via the Zig FFI.
+* The haptic intensity is proportional to the stability drop.
+* This is a side effect managed entirely by the interpreter — not
+visible in the Error-Lang type system.
+
+==== No User-Defined Effects
+
+* Error-Lang does not expose an effect system to users.
+* All effects are implicit and managed by the interpreter runtime.
+* This is intentional: the language teaches through experience, not
+abstraction.
+
+'''''
+
+=== Module System
+
+Error-Lang has no explicit module system.
+
+==== Design Rationale
+
+* Modules add cognitive overhead for beginners.
+* Error-Lang programs are small (typically < 100 lines) and
+self-contained.
+* The focus is on understanding individual errors, not software
+architecture.
+
+==== File Execution
+
+* Each `+.err+` file is an independent program.
+* No imports, no exports, no namespaces.
+* The standard library (error constructors, stability queries) is always
+available without import.
+
+==== Built-in Functions (Always Available)
+
+[width="100%",cols="31%,69%",options="header",]
+|===
+|Function |Description
+|`+stability()+` |Returns current stability score
+|`+paradox_depth()+` |Returns current paradox nesting level
+|`+error_count()+` |Returns total errors in this session
+|`+hint()+` |Requests a contextual hint
+|`+intentional(expr)+` |Marks an expression as a deliberate error
+|`+history()+` |Returns the error history for this session
+|===
+
+==== Compiler Organisation (Internal)
+
+* The AffineScript compiler is a single package (not split into
+sub-packages).
+* Source files: `+Lexer.res+`, `+Parser.res+`, `+Interpreter.res+`,
+`+Stability.res+`, `+HapticsBridge.res+`.
+* The Zig FFI is a single `+haptics.zig+` file compiled to a shared
+library.
diff --git a/spec/system-specs.md b/spec/system-specs.md
deleted file mode 100644
index 6e3887d..0000000
--- a/spec/system-specs.md
+++ /dev/null
@@ -1,160 +0,0 @@
-
-# SPDX-License-Identifier: CC-BY-SA-4.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
-
-# Error-Lang System Specifications
-
-Error-Lang is a pedagogical programming language where errors are features.
-Implementation stack: AffineScript compiler (compiles to JavaScript), Zig FFI for
-computational haptics feedback. Designed for learning through deliberate failure.
-
----
-
-## Memory Model
-
-Error-Lang's memory model is intentionally simple, befitting its pedagogical
-purpose, with a specialised FFI layer for haptics.
-
-### JavaScript Runtime (Primary)
-
-- AffineScript compiles to JavaScript; all Error-Lang values are JS heap objects
- managed by the JavaScript engine's garbage collector.
-- No manual memory management is exposed to Error-Lang users.
-- Values are immutable by default (AffineScript's functional core).
-- Mutable state is limited to the interpreter's internal bookkeeping.
-
-### Interpreter State
-
-- The interpreter maintains a `StabilityState` struct containing:
- - **stability_score**: `float` — current program stability (0.0 to 1.0).
- - **paradox_level**: `int` — depth of active paradox nesting.
- - **error_history**: `array` — log of all errors encountered.
- - **correction_attempts**: `int` — number of user fix attempts this session.
-- This state persists across statements within a single REPL session or file
- execution and is reset between sessions.
-
-### Zig FFI Layer (Computational Haptics)
-
-- The Zig FFI module manages its own memory via `std.mem.Allocator`.
-- Haptic feedback buffers are allocated per-event and freed after transmission
- to the haptic device.
-- No GC interaction — Zig allocations are invisible to the JS runtime.
-- Data crossing the FFI boundary is serialised to C-compatible structs defined
- in `generated/abi/haptics.h`.
-
-### Memory Invariants
-
-- Error-Lang programs cannot cause memory leaks in user-space (GC handles all).
-- Zig FFI allocations are bounded: at most one haptic buffer active at a time.
-- The stability state struct has a fixed, small memory footprint.
-
----
-
-## Concurrency Model
-
-Error-Lang is deliberately single-threaded.
-
-### Design Rationale
-
-- Concurrency adds complexity that conflicts with pedagogical goals.
-- Learners should focus on understanding errors and stability, not race
- conditions or deadlocks.
-- The single-threaded model makes program behaviour fully deterministic
- (modulo stability score thresholds).
-
-### Execution Model
-
-- Statements execute sequentially in source order.
-- The REPL processes one input at a time, updating stability state after each.
-- No async operations, no event loop, no callbacks.
-
-### Haptic Feedback Timing
-
-- Zig FFI calls for haptic feedback are synchronous and blocking.
-- Haptic events are brief (< 50ms) so blocking is imperceptible.
-- If no haptic device is connected, the FFI call returns immediately (no-op).
-
----
-
-## Effect System
-
-Error-Lang's effect system is unconventional: stability impact and paradox
-state are the primary tracked effects.
-
-### Stability as Effect
-
-Every statement in Error-Lang has a stability impact:
-
-| Category | Stability Effect | Example |
-|---------------------|--------------------------|----------------------------------|
-| Correct statement | `+0.05` to `+0.10` | Valid assignment, correct logic |
-| Syntax error | `-0.15` to `-0.25` | Missing semicolon, bad indent |
-| Type error | `-0.10` to `-0.20` | Wrong argument type |
-| Deliberate error | `+0.02` (learning bonus) | Annotated with `@intentional` |
-| Error correction | `+0.15` to `+0.20` | Fixing a previous error |
-| Repeated error | `-0.30` (penalty) | Same error class within 5 stmts |
-
-- Stability is checked implicitly after every statement.
-- When stability drops below `0.2`, the interpreter enters "crisis mode" —
- haptic feedback intensifies and hints become more explicit.
-- When stability reaches `1.0`, the session is "mastered."
-
-### Paradox State as Implicit Effect
-
-- Certain constructs create paradoxes (self-referential errors, contradictions).
-- Paradox depth is tracked as an implicit effect counter.
-- Paradoxes cannot be nested beyond depth 3 (interpreter rejects deeper nesting).
-- Resolving a paradox grants a significant stability bonus (`+0.25`).
-
-### Haptic Effect
-
-- Error events trigger haptic feedback via the Zig FFI.
-- The haptic intensity is proportional to the stability drop.
-- This is a side effect managed entirely by the interpreter — not visible in
- the Error-Lang type system.
-
-### No User-Defined Effects
-
-- Error-Lang does not expose an effect system to users.
-- All effects are implicit and managed by the interpreter runtime.
-- This is intentional: the language teaches through experience, not abstraction.
-
----
-
-## Module System
-
-Error-Lang has no explicit module system.
-
-### Design Rationale
-
-- Modules add cognitive overhead for beginners.
-- Error-Lang programs are small (typically < 100 lines) and self-contained.
-- The focus is on understanding individual errors, not software architecture.
-
-### File Execution
-
-- Each `.err` file is an independent program.
-- No imports, no exports, no namespaces.
-- The standard library (error constructors, stability queries) is always
- available without import.
-
-### Built-in Functions (Always Available)
-
-| Function | Description |
-|---------------------|------------------------------------------------|
-| `stability()` | Returns current stability score |
-| `paradox_depth()` | Returns current paradox nesting level |
-| `error_count()` | Returns total errors in this session |
-| `hint()` | Requests a contextual hint |
-| `intentional(expr)` | Marks an expression as a deliberate error |
-| `history()` | Returns the error history for this session |
-
-### Compiler Organisation (Internal)
-
-- The AffineScript compiler is a single package (not split into sub-packages).
-- Source files: `Lexer.res`, `Parser.res`, `Interpreter.res`, `Stability.res`,
- `HapticsBridge.res`.
-- The Zig FFI is a single `haptics.zig` file compiled to a shared library.
diff --git a/spec/type-system.md b/spec/type-system.adoc
similarity index 51%
rename from spec/type-system.md
rename to spec/type-system.adoc
index a1915f3..a2988df 100644
--- a/spec/type-system.md
+++ b/spec/type-system.adoc
@@ -1,20 +1,16 @@
-
-# SPDX-License-Identifier: CC-BY-SA-4.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
+== SPDX-License-Identifier: CC-BY-SA-4.0
-# Error-Lang Type System: Quantum Type Superposition
+== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk
-**Version:** 1.0.0
-**Date:** 2026-03-14
+== Error-Lang Type System: Quantum Type Superposition
----
+*Version:* 1.0.0 *Date:* 2026-03-14
-## 1. Type Language
+'''''
-```
+=== 1. Type Language
+
+....
τ ::= Int | Float | String | Bool primitive types
| Nil void/nil
| [τ] array
@@ -24,28 +20,28 @@ Copyright (c) Jonathan D.A. Jewell
| EchoR<τₐ, τᵦ> echo residue (witness erased)
| Any wildcard (unifies with all)
| α type variable (unification)
-```
+....
----
+'''''
-## 2. Quantum Types
+=== 2. Quantum Types
-### 2.1 Quantum State
+==== 2.1 Quantum State
Variables in Error-Lang exist in one of two states:
-```
+....
Q ::= Collapsed(τ) type determined
| Superposition(possible: [τ₁,…,τₙ], seed: ℤ, loc: Loc)
type undetermined
-```
+....
-### 2.2 Superposition Assignment
+==== 2.2 Superposition Assignment
-When a variable is declared **without** a type annotation, its type enters
-superposition based on the literal's possible interpretations:
+When a variable is declared *without* a type annotation, its type enters
+superposition based on the literal’s possible interpretations:
-```
+....
annotation = None lit = IntLit
──────────────────────────────────────────────────── [Q-Int]
Q(x) = Superposition([Int, Float, String], seed, loc)
@@ -61,36 +57,38 @@ superposition based on the literal's possible interpretations:
annotation = None lit = BoolLit
────────────────────────────────────────────────── [Q-Bool]
Q(x) = Superposition([Bool, Int, String], seed, loc)
-```
+....
-### 2.3 Annotation Prevents Superposition
+==== 2.3 Annotation Prevents Superposition
-```
+....
annotation = Some(τ)
────────────────────────────── [Q-Annotated]
Q(x) = Collapsed(τ) (immediate, no superposition)
-```
+....
----
+'''''
-## 3. Wavefunction Collapse
+=== 3. Wavefunction Collapse
-### 3.1 Observation Contexts
+==== 3.1 Observation Contexts
There are six observation contexts, each assigned a hash value:
-| Context | Hash | Trigger |
-|---------|------|---------|
-| Arithmetic | 0 | `x + y`, `x - y`, `x * y`, `x / y` |
-| StringOp | 1 | `x ++ y`, string interpolation |
-| Comparison | 2 | `x == y`, `x < y`, etc. |
-| Print | 3 | `println(x)` |
-| Assignment | 4 | `let y: T = x` (assigned to typed variable) |
-| FunctionArg | 5 | `f(x)` where parameter has type annotation |
+[cols=",,",options="header",]
+|===
+|Context |Hash |Trigger
+|Arithmetic |0 |`+x + y+`, `+x - y+`, `+x * y+`, `+x / y+`
+|StringOp |1 |`+x ++ y+`, string interpolation
+|Comparison |2 |`+x == y+`, `+x < y+`, etc.
+|Print |3 |`+println(x)+`
+|Assignment |4 |`+let y: T = x+` (assigned to typed variable)
+|FunctionArg |5 |`+f(x)+` where parameter has type annotation
+|===
-### 3.2 Collapse Algorithm
+==== 3.2 Collapse Algorithm
-```
+....
collapse(Q, context) =
match Q with
| Collapsed(τ) → τ (already collapsed)
@@ -99,30 +97,31 @@ collapse(Q, context) =
τ = possible[hash]
Q ← Collapsed(τ) (mutate to collapsed)
τ
-```
+....
-### 3.3 Determinism Guarantee
+==== 3.3 Determinism Guarantee
-Given the same `seed` and `context`, collapse always produces the same type.
-Seeds are derived from the variable's declaration location and the run counter:
+Given the same `+seed+` and `+context+`, collapse always produces the
+same type. Seeds are derived from the variable’s declaration location
+and the run counter:
-```
+....
seed = hash(source_file, line, column, run_counter)
-```
+....
-This means:
-- **Within a run:** Deterministic (same program, same types)
-- **Across runs:** May differ (different run_counter → different seed → different collapse)
+This means: - *Within a run:* Deterministic (same program, same types) -
+*Across runs:* May differ (different run_counter → different seed →
+different collapse)
----
+'''''
-## 4. Standard Type Checking
+=== 4. Standard Type Checking
-### 4.1 Unification
+==== 4.1 Unification
-Error-Lang uses Robinson's unification for non-quantum types:
+Error-Lang uses Robinson’s unification for non-quantum types:
-```
+....
unify(τ₁, τ₂) =
| Ok(∅) if τ₁ = τ₂
| Ok({α ↦ τ₂}) if τ₁ = α, no occurs check failure
@@ -130,11 +129,11 @@ unify(τ₁, τ₂) =
| Ok(∅) if τ₁ = Any or τ₂ = Any
| unify_structure for functions, arrays (recursive)
| Err(Mismatch) otherwise
-```
+....
-### 4.2 Typing Rules
+==== 4.2 Typing Rules
-```
+....
────────────────── [T-Int] ────────────────── [T-Bool]
Γ ⊢ n : Int Γ ⊢ b : Bool
@@ -160,15 +159,15 @@ unify(τ₁, τ₂) =
Γ ⊢ f : (τ₁,…,τₙ) → τᵣ ∀i. Γ ⊢ aᵢ : τᵢ
────────────────────────────────────────────────── [T-Call]
Γ ⊢ f(a₁, …, aₙ) : τᵣ
-```
+....
----
+'''''
-## 5. Stability Impact of Types
+=== 5. Stability Impact of Types
Type-related stability penalties:
-```
+....
Q(x) = Superposition(…) (variable in superposition)
────────────────────────────────────────────────────── [Stab-Super]
stability -= 15 (TypeInstability penalty)
@@ -180,49 +179,56 @@ Type-related stability penalties:
e : Echo echo_to_residue(e) : EchoR
────────────────────────────────────────────────────── [Stab-Erase]
stability -= 15 (erasure of a witness is a thermodynamic act)
-```
+....
-See §7 for Echo types. The `[Stab-Erase]` rule is Error-Lang's signature move:
-structured loss is permitted, but **structure is not free** — collapsing an `Echo`
-to its `EchoR` residue destroys the input witness and incurs a Landauer-style debit
-(cf. `fiber_erasure_bound` in the EchoTypes.jl companion).
+See §7 for Echo types. The `+[Stab-Erase]+` rule is Error-Lang’s
+signature move: structured loss is permitted, but *structure is not
+free* — collapsing an `+Echo+` to its `+EchoR+` residue destroys the
+input witness and incurs a Landauer-style debit
+(cf. `+fiber_erasure_bound+` in the EchoTypes.jl companion).
----
+'''''
-## 6. Properties
+=== 6. Properties
-1. **Collapse determinism:** Given same seed and context, same type is selected.
-2. **Annotation safety:** Type annotations prevent superposition entirely.
-3. **Pedagogical monotonicity:** Annotations always improve stability (never penalised).
-4. **Gradual typing compatible:** `Any` unifies with everything, enabling partial typing.
-5. **No implicit narrowing:** Numeric widening only (Int → Float, never Float → Int).
-6. **Erasure irreversibility:** `Echo` does not unify with `EchoR`; once a
- witness is erased, the residue cannot be used where a recoverable echo is required.
+[arabic]
+. *Collapse determinism:* Given same seed and context, same type is
+selected.
+. *Annotation safety:* Type annotations prevent superposition entirely.
+. *Pedagogical monotonicity:* Annotations always improve stability
+(never penalised).
+. *Gradual typing compatible:* `+Any+` unifies with everything, enabling
+partial typing.
+. *No implicit narrowing:* Numeric widening only (Int → Float, never
+Float → Int).
+. *Erasure irreversibility:* `+Echo+` does not unify with
+`+EchoR+`; once a witness is erased, the residue cannot be used
+where a recoverable echo is required.
----
+'''''
-## 7. Echo Types (Structured Loss)
+=== 7. Echo Types (Structured Loss)
-Echo types give Error-Lang a first-class, runnable model of **structured loss** —
-*non-total erasure* — adapted from the constructive Agda library
-[`echo-types`](https://github.com/hyperpolymath/echo-types) and its finite,
-executable companion
-[`EchoTypes.jl`](https://github.com/hyperpolymath/EchoTypes.jl).
+Echo types give Error-Lang a first-class, runnable model of *structured
+loss* — _non-total erasure_ — adapted from the constructive Agda library
+https://github.com/hyperpolymath/echo-types[`+echo-types+`] and its
+finite, executable companion
+https://github.com/hyperpolymath/EchoTypes.jl[`+EchoTypes.jl+`].
-### 7.1 Formation
+==== 7.1 Formation
-For a (conceptual) function `f : A → B` and an output `y : B`, the *echo* is the
-**fibre** of `f` over `y`: the proof-relevant collection of inputs that reach `y`.
-In Agda:
+For a (conceptual) function `+f : A → B+` and an output `+y : B+`, the
+_echo_ is the *fibre* of `+f+` over `+y+`: the proof-relevant collection
+of inputs that reach `+y+`. In Agda:
-```
+....
Echo f y := Σ (x : A) , (f x ≡ y)
-```
+....
-Error-Lang surfaces this as a type constructor indexed by the domain `A` and
-codomain `B`:
+Error-Lang surfaces this as a type constructor indexed by the domain
+`+A+` and codomain `+B+`:
-```
+....
A type B type
────────────────────── [T-Echo]
Echo type
@@ -230,82 +236,104 @@ codomain `B`:
Sugar:
Echo ≡ Echo (codomain inferred — treated as Any)
Echo ≡ Echo (opaque fallback / unresolved)
-```
+....
-A runtime echo value is a **single fibre witness** `VEcho{input, output}`: one `x`
-that reached `y`. (The whole-fibre `fiber(f, domain, y)` of EchoTypes.jl awaits
-first-class functions in the VM; the witness is the faithful runtime compromise.)
+A runtime echo value is a *single fibre witness*
+`+VEcho{input, output}+`: one `+x+` that reached `+y+`. (The whole-fibre
+`+fiber(f, domain, y)+` of EchoTypes.jl awaits first-class functions in
+the VM; the witness is the faithful runtime compromise.)
-### 7.2 Residue and erasure
+==== 7.2 Residue and erasure
-`echo_to_residue` weakens an echo to its **residue** `EchoR`: the input
-witness is **erased** (non-recoverable); only reachability of the output `y : B`
-is retained. This is the operational meaning of *structured loss* — the output
-constraint survives, the witness does not.
+`+echo_to_residue+` weakens an echo to its *residue* `+EchoR+`:
+the input witness is *erased* (non-recoverable); only reachability of
+the output `+y : B+` is retained. This is the operational meaning of
+_structured loss_ — the output constraint survives, the witness does
+not.
-```
+....
Γ ⊢ e : Echo
────────────────────────────────── [T-Erase]
Γ ⊢ echo_to_residue(e) : EchoR (+ [Stab-Erase], §5)
-```
+....
-### 7.3 Unification
+==== 7.3 Unification
-`Echo` and `EchoR` unify structurally with their own kind, component-wise, and
-**never with each other** — encoding the irreversibility of erasure in the type
-system itself:
+`+Echo+` and `+EchoR+` unify structurally with their own kind,
+component-wise, and *never with each other* — encoding the
+irreversibility of erasure in the type system itself:
-```
+....
unify(Echo, Echo) = unify(A₁,A₂) ∧ unify(B₁,B₂)
unify(EchoR, EchoR) = unify(A₁,A₂) ∧ unify(B₁,B₂)
unify(Echo<…>, EchoR<…>) = ✗ (residue is not a recoverable echo)
-```
+....
+
+==== 7.4 Builtins
+
+Named to mirror EchoTypes.jl, so concepts map 1:1 across the three
+codebases:
+
+[width="100%",cols="34%,33%,33%",options="header",]
+|===
+|Builtin |Type |Meaning
+|`+echo(x, y)+` |`+(A, B) → Echo+` |construct a fibre witness:
+`+x+` reached `+y+`
+
+|`+echo_to_residue(e)+` |`+Echo → EchoR+` |erase the witness
+(incurs `+[Stab-Erase]+`)
-### 7.4 Builtins
+|`+residue_strictly_loses(r)+` |`+EchoR → Bool+` |witness
+non-recoverability
-Named to mirror EchoTypes.jl, so concepts map 1:1 across the three codebases:
+|`+echo_input(e)+` |`+Echo → A+` |recover the witness — *illegal
+on a residue*
-| Builtin | Type | Meaning |
-|---|---|---|
-| `echo(x, y)` | `(A, B) → Echo` | construct a fibre witness: `x` reached `y` |
-| `echo_to_residue(e)` | `Echo → EchoR` | erase the witness (incurs `[Stab-Erase]`) |
-| `residue_strictly_loses(r)` | `EchoR → Bool` | witness non-recoverability |
-| `echo_input(e)` | `Echo → A` | recover the witness — **illegal on a residue** |
-| `echo_output(e)` | `Echo \| EchoR → B` | the retained output (survives erasure) |
+|`+echo_output(e)+` |`+Echo \| EchoR → B+` |the retained
+output (survives erasure)
+|===
-`echo_input` on an `EchoR` is a **type error** (and a runtime error): the witness
-is gone. This is the type system enforcing that loss, once structured, is real.
+`+echo_input+` on an `+EchoR+` is a *type error* (and a runtime error):
+the witness is gone. This is the type system enforcing that loss, once
+structured, is real.
-### 7.5 Decomposition obligations (decomposition must be visible)
+==== 7.5 Decomposition obligations (decomposition must be visible)
-Error-Lang is a *decompositional* language: Echo's correctness is not "Echo
-typechecks" but "the code's decomposition behaviour is represented syntactically,
-semantically, and in type checking." The governing invariant is:
+Error-Lang is a _decompositional_ language: Echo’s correctness is not
+"`Echo typechecks`" but "`the code’s decomposition behaviour is
+represented syntactically, semantically, and in type checking.`" The
+governing invariant is:
-> **Decomposition must be visible.** `echo_to_residue` is never a silent cast;
-> `EchoR` never behaves as an `Echo` with a missing field; the stability debit is
-> never hidden in incidental runtime behaviour.
+____
+*Decomposition must be visible.* `+echo_to_residue+` is never a silent
+cast; `+EchoR+` never behaves as an `+Echo+` with a missing field; the
+stability debit is never hidden in incidental runtime behaviour.
+____
Echo is therefore specified and tested across three planes:
-1. **Syntactic** — parse/pretty-print round-trip for `Echo`/`EchoR`; malformed
- Echo fails clearly; sugar lowers predictably (§7.1); nested forms
- (`Echo>`) survive the greedy `>>` lexing.
-2. **Semantic / runtime** — `echo` builds `VEcho{input,output}`; `echo_input`
- works on `VEcho` and fails on `VResidue`; `echo_output` works on both;
- `echo_to_residue` yields `VResidue` and the witness becomes genuinely
- unavailable; `residue_strictly_loses` reports non-recoverability; stability is
- debited **exactly once** by `echo_to_residue` and **never** by projection.
-3. **Type-checking** — the unification and builtin rules of §7.3–§7.4, including
- `EchoR` not unifying back into `Echo` and no implicit `Echo → EchoR` or
- `Echo → B` coercion.
-
-See `docs/Echo-Decomposition.adoc` for the narrative form of these obligations.
-
-### 7.6 Fidelity note
-
-Error-Lang is a runnable scripting language, not a proof assistant: the equality
-proof `f x ≡ y` is carried as a runtime-checkable pairing, not a HoTT path. The
-`echo-types` Agda library remains the source of mechanized truth; `EchoTypes.jl`
-is the executable finite-domain model; Error-Lang's `Echo`/`EchoR` are the
-operational, stability-aware embedding of the same lineage.
+[arabic]
+. *Syntactic* — parse/pretty-print round-trip for `+Echo+`/`+EchoR+`;
+malformed Echo fails clearly; sugar lowers predictably (§7.1); nested
+forms (`+Echo>+`) survive the greedy `+>>+` lexing.
+. *Semantic / runtime* — `+echo+` builds `+VEcho{input,output}+`;
+`+echo_input+` works on `+VEcho+` and fails on `+VResidue+`;
+`+echo_output+` works on both; `+echo_to_residue+` yields `+VResidue+`
+and the witness becomes genuinely unavailable;
+`+residue_strictly_loses+` reports non-recoverability; stability is
+debited *exactly once* by `+echo_to_residue+` and *never* by projection.
+. *Type-checking* — the unification and builtin rules of §7.3–§7.4,
+including `+EchoR+` not unifying back into `+Echo+` and no implicit
+`+Echo → EchoR+` or `+Echo → B+` coercion.
+
+See `+docs/Echo-Decomposition.adoc+` for the narrative form of these
+obligations.
+
+==== 7.6 Fidelity note
+
+Error-Lang is a runnable scripting language, not a proof assistant: the
+equality proof `+f x ≡ y+` is carried as a runtime-checkable pairing,
+not a HoTT path. The `+echo-types+` Agda library remains the source of
+mechanized truth; `+EchoTypes.jl+` is the executable finite-domain
+model; Error-Lang’s `+Echo+`/`+EchoR+` are the operational,
+stability-aware embedding of the same lineage.