BANG → v1 · North-Star Roadmap
⚠️ K-keyframe roadmap — predates ADR-0016 (third design revision). K0-K3 milestones (effect-row oracle; reference
eval; calculated machines) all landed and remain the research narrative. K4+ keyframes have been REPLACED by the two-hop architecture of ADR-0016 (graded-CBPV → CalcVM → WasmFX) and the ◊-checkpoint progression inROADMAP.md.READING ORDER: this doc for the research narrative + intellectual lineage;
ROADMAP.mdfor the orchestrator's current map;CLAUDE.md→CONTEXT.mdfor current state;docs/decisions/0016-*.mdfor the architecture in force.Drift from the original:
- Effect TS / WasmFX as "K5 optional lowerings" gone. WasmFX is the primary compiler target per ADR-0016.
- Harness retired (TS differential tests deleted with the wasmfx merge; the standing gate is now
Bang/Audit.leanper Phase B PROOF_ORDER).oracle-lean/Bang/...paths are nowBang/...(post-flatten; see commit4a1b7a4).Keyframes are committed poses (states that must hold). Inbetweens are implementation, drawn later. Proof rides the reference; the shipping path is kept honest by the harness; performance is summoned only when it touches the user; the machine is an output of the calculation, never hand-designed.
Status: K0 locked · K1 done · K2 done (the pure core calculated + proven across 4 increments) · K3 in progress (Throws + State calculated + proven, both composed with the closure/CBN core, both together in one machine — CalcCBNEffSt; and the reification frontier reached — CalcReify, a flat generalised-continuation machine for multi-shot/non-tail handlers, machine + 7 rfl-verified demonstrators, its general theorem the named next step. runState×throw and a user-extensible effect set still open). Eight machines fully proven + the reification machine validated, zero sorrys (asserts only what it proves). Live detail: AGENTS.md "Current playhead".
0 · Locked v0 decisions
| # | decision | was | now | why |
|---|---|---|---|---|
| D1 | reactivity | let sig keyword | mut + operator | : introduces (silent), = updates (notifies subscribers); collapses declare/assign/create-signal/update → 2 operators |
| D2 | binding forms | let / mut / sig / tvar | let / mut / tvar | sig absorbed by D1 → kernel shrinks |
| D3 | capture | implicit lexical | explicit & tracked | thunks trivially serializable → distribution + durable exec; deps fully visible; simpler calculated closures |
| D4 | canonical target | Effect TS transpile (MVP) | calculated VM (owned) | own the runtime; correct-by-construction; ecosystem-independent |
| D5 | Effect TS / Koka-CPS / WasmFX | the backend | optional K5 lowerings | demoted: foundation → fast-path |
| D6 | STM | privileged kernel primitive | unchanged — axiomatized in VM, not derived | journal/retry/conflict needs runtime support; "everything is a handler" has exactly this one ceiling |
Force is $ (prefix); parens group without forcing. Bare name = description; $name = value. ! is freed for actor-send. (Superseded the earlier !-as-force note — see ADR-0007, which is the source of truth.)
1 · Keyframe arc
| frame | pose | invariant that holds | proves | runs | status |
|---|---|---|---|---|---|
| K0 | model sheet | core semantics in Lean: thunk · $ force · rows-as-sets · 1-shot handlers · STM; D1–D6 baked in | model sheet typechecks | core programs, interpreted | ✅ locked |
| K1 | oracle speaks | reference is executable; unifier verified (Finset semilattice); harness drives candidates | unify_sound; laws inherited | harness · 20k cases green | ✅ done |
| K2 | machine falls out | Bahr–Hutton derives (compile, Code, exec) from eval; pure core done — arithmetic → let/var → CBV closures → CBN+$force, all proven exec ∘ compile ≡ eval (Calc/CalcHO/CalcCBN) | exec ∘ compile ≡ eval | core BANG on owned machine | ✅ proven (fuel, not partiality monad) |
| K3 | effects on the machine | per-effect calculated machines: Throws → handler stack + unwinding (CalcEff), State → threaded register (CalcSt), both proven; both composed with the closure/CBN core — CalcCBNEff + CalcCBNSt, and both together in one machine (CalcCBNEffSt, the effect-row model, State persists through a throw), proven; handler stack → config, effect ops → instructions; STM axiomatized | correctness over the effect monad | effectful BANG end-to-end | 🟡 Throws+State proven · composed with closures, proven · both-at-once proven · reification + runState×throw open |
| K4 | front end is real | parse → typed AST → effect-row inference (on the verified unifier) → core IR | inference soundness via oracle | real .bang files | ⬜ |
| K5 | fast path (optional) | optimized bytecode interp (C/Rust/Zig) and/or calculated lowering → C·Wasm·WasmFX·Effect TS; diff-tested vs exec | lowering refines exec | UX-acceptable speed · portable | ⬜ |
| K6 | toolchain eats itself | build = thunk graph (targets=thunks, deps=R, incremental=content-addressed memo); BANG-native | rebuild ⟺ inputs changed | BANG builds BANG | ⬜ |
| K7 | v1 / north star | syntax + effect-typed front end + verified core runtime + fast path + native build; harness standing | the chain holds frame→frame | something worth running (HMS constraint-evaluator slice) | ⭐ |
2 · Architecture (what depends on what)
- Reference (proven):
eval→ oracle → calculated VM. Changes rarely; no per-session babysitting. - Shipping (tested, not proven against): lowerings + front end, kept honest by the harness.
- Invariant: anything that runs is either
execitself or differential-tested against it.
3 · The calculation (K2–K3 mechanics)
Staging — each a calculated (compiler, machine) pair; composition gives end-to-end correctness:
- Pure core → derive VM for thunk +
$force + application. (template: Calculating Dependently-Typed Compilers, Lean-shaped) - + Effects → swap underlying monad to the effect-row monad. (Monadic Compiler Calculation)
- + Divergence → partiality monad + bisimilarity. ⚠ Lean's coinduction is the effortful spot.
- + Concurrency/STM → STM as machine primitives, not derived. (Calculating Compilers for Concurrency)
- Frontier (post-v1): multi-shot handlers (machine must reify continuations) → defer.
The VM is the output of step 1–4. Pre-committing to a VM design and justifying a compiler against it = CompCert mode = more work, none of the elegance.
4 · Kernel vs library = the VM contract
The design doc's kernel/library split is the machine's primitive/library boundary.
| layer | contents |
|---|---|
| kernel (VM must provide natively) | thunks · force · application · effect rows + handler dispatch · pattern matching + ADTs · STM (journal, conflict detection, retry) |
| library (ordinary BANG over the kernel) | State/IO/Throws · Reactive+signals · Spawn/Send/Receive+actors · async/await · logging/metrics/tracing · all runtimes (thread pools, event loops, green threads, deterministic schedulers) · all STM-built concurrency (channels, semaphores, futures, queues) |
→ K2/K3 acceptance test = "the kernel column is native; the library column compiles to ordinary code."
5 · Effect-row model (already formalized, K1)
| concept | model | Lean | law source |
|---|---|---|---|
| label set | idempotent set | Finset ℕ | — |
| compose | union = join | ∪ (= ⊔) | Mathlib Lattice |
| empty | bottom | ∅ (= ⊥) | OrderBot |
| canonical ⟺ equal | extensional eq | Finset.ext | free (was the F* keystone) |
open row ...e | set + tail var | { labels, tail : Option RVar } | unify |
Unification (sound, not principal — MGU deferred to differential test):
- closed ⋈ closed → equal sets, else fail
- open ⋈ closed → require
open ⊆ closed; bind tail ←closed \ open(closed) - open ⋈ open → fresh tail
f; bind each tail ← other'sdiff, tailf
→ This is the answer to the spec's open question "row variables with IO, ...e". We're ahead of the spec on the semantics; only surface syntax + infer-vs-annotate policy remain.
6 · Open forks still live (post-collapse)
| fork | options | current lean |
|---|---|---|
| capture syntax | C++ [x,&y] / Rust move / Swift [weak]-style lists | explicit list, TBD spelling |
| serializability | tracked effect · type-class constraint · content-address-derived | content-address-derived |
| module constants | explicit-pass vs free-to-reference | free (immutable, content-addressed, cheap to ship) |
| STM ⊂ reversibility? | STM beside vs STM = a built-in reversible region | post-v1 seam (could absorb D6's exception) |
| effect inference scope | infer-all vs infer-internal/annotate-boundaries | infer internal, annotate at module boundary |
| transaction + IO | forbid vs unsafePerformIO-style escape | forbid by default (retry ⇒ IO must be reversible) |
7 · Frontier (beyond v1)
- Reversibility / groupoids. Opt-in
reversibleeffect/region; ops carry inverses. Buys time-travel debugging, undo-as-primitive, clean speculative rollback, bidirectional transforms. → STM becomes a special case of a reversible region with a conflict policy. Potentially simplifies the kernel (one privileged mechanism: reversible regions) rather than special-casing STM. Inverse likely lives in the handler, not the operation (different handlers compensate differently). - Distributed eval. Ship bare
name(description, small) not$name(value, big); force at the data. Enabled by D3 (no implicit capture → serializable thunks). - Native multi-shot handlers. The hard machine extension; reify continuations.
8 · Reading canon — calculating correct compilers
PDFs: cs.nott.ac.uk/~pszgmh/bib.html · bahr.io/pubs. Read 2015 → 2017 → 2021 → 2022 → 2023.
| year | paper | why for BANG |
|---|---|---|
| 1967 | McCarthy & Painter — Correctness of a Compiler for Arithmetic Expressions | the origin; everything is a reply to it |
| 2004 | Hutton & Wright — Compiling Exceptions Correctly · Calculating an Exceptional Machine | where calculate ≠ verify begins (defunctionalization) |
| 2015 | Bahr & Hutton — Calculating Correct Compilers (JFP 25) | the method. start here. Coq-formalized |
| 2016 | Hutton & Bahr — Cutting Out Continuations | the CPS intuition, in miniature |
| 2017 | Hutton & Bahr — Compiling a 50-Year Journey (JFP 27) | the map / retrospective |
| 2020 | Bahr & Hutton — Calculating Correct Compilers II: Register Machines (JFP 30) | generalizes off the stack |
| 2021 | Pickard & Hutton — Calculating Dependently-Typed Compilers (ICFP) | your Lean blueprint — intrinsically typed |
| 2022 | Bahr & Hutton — Monadic Compiler Calculation (ICFP) | the hook for effects — swap the monad; partiality for divergence |
| 2023 | Bahr & Hutton — Calculating Compilers for Concurrency (ICFP) | nearest BANG's fibers + STM |
| 2024 | Garby, Hutton & Bahr — Calculating Compilers Effectively (Haskell) | emit efficient, not tree-shaped, code |
| 2024 | Bahr & Hutton — Beyond Trees: Graph-Based Compilers (ICFP) | jumps / graph-structured code (HOAS) |
| 2024 | Tsuyama et al. — An Intrinsically Typed Compiler for Algebraic Effect Handlers (PEPM) | adjacent + vital — handlers → typed stack machine, in Agda; closest artifact to K3 |
| — | Geeson (Oxford MSc) — Calculating Compilers and Algebraic Effects | worked precedent: method × effects, CBPV+exceptions |
keyframes committed · inbetweens to be drawn · next pose to lock: K2