|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | +// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) |
| 4 | += betlang — Core Build Plan (core → post-core tier) |
| 5 | +:toc: |
| 6 | +:sectnums: |
| 7 | + |
| 8 | +The level-by-level plan to bring betlang to *absolutely core* — a single-identity |
| 9 | +language that **runs real probabilistic programs end to end** — followed by the |
| 10 | +post-core tier (native compile + inference + coprocessor acceleration). Companion |
| 11 | +to link:2026-06-15-betlang-wiring-and-bet-dist-t.adoc[the wiring/bet:Dist T ADR log]. |
| 12 | + |
| 13 | +== Definition of "absolutely core" |
| 14 | + |
| 15 | +____ |
| 16 | +You write a real betlang program in ONE canonical syntax, and `bet check` + |
| 17 | +`bet run` parse it, type-check it (`bet : Dist T`), and **interpret it correctly |
| 18 | +end to end** — distributions and a minimal stdlib are callable, type errors are |
| 19 | +real errors, and a conformance corpus in that syntax is green in CI. The Lean |
| 20 | +proof certifies the typed core on top of that. |
| 21 | +____ |
| 22 | + |
| 23 | +Everything else — extra backends, native compile, full PPL inference, the meta |
| 24 | +layer, Julia/aLib/StatistEase, the analytic/FFI/concurrency proofs — is *post-core*. |
| 25 | + |
| 26 | +== Locked architecture decisions (from the 2026-06-15 design pass) |
| 27 | + |
| 28 | +* *One production language: Rust.* Front-end (parse/check/AST), interpreter, the |
| 29 | + `bet-rt` runtime, and the eventual native backend are all Rust. No polyglot |
| 30 | + production pipeline (avoids a cross-language seam / interstitial drift). |
| 31 | +* *Two execution tiers.* **Iterate** = tree-walking interpreter (core). **Deploy** |
| 32 | + = compile (post-core). Don't put a compiler on the iterate path. |
| 33 | +* *World B (native).* Native x86_64 via **Cranelift** (pure-Rust, fast, JIT-capable); |
| 34 | + inference offloaded to **Julia (Turing.jl) + Axiom.jl**; *not* .NET. (Rejected: |
| 35 | + betlang→.NET/Infer.NET — would be a second runtime; .NET's own JIT makes Cranelift |
| 36 | + redundant in that world. Rejected: F# as a production stage — second runtime, |
| 37 | + can't share `bet-rt` or feed Cranelift.) |
| 38 | +* *F# = optional prototyping/reference lane, off the shipped path.* Use `dotnet fsi` |
| 39 | + to sketch a new semantics, then port the settled design to Rust. Never shipped. |
| 40 | + (The estate's sanctioned ML-compiler lane is OCaml; the Lean model + legacy Racket |
| 41 | + core already partly occupy the "reference oracle" niche.) |
| 42 | +* *Two seams: design EARLY, build LATE.* |
| 43 | + ** an *effect-handler seam* for `sample`/`observe` in the interpreter — this is |
| 44 | + what a metainterpreter (= the inference engine) plugs into; |
| 45 | + ** a *typed coprocessor `Handle`/`Bridge`* (AffineScript pattern: `NotReady → |
| 46 | + Ready(Bridge)`) routing numeric kernels to **Axiom.jl** (Julia → Zig SIMD → |
| 47 | + GPU, self-healing fallback). |
| 48 | +* *Metacompiler:* only the *grammar → parser generation* slice is in scope (post-L1, |
| 49 | + to kill spec/impl drift). Full staging / partial-evaluation is deferred. |
| 50 | + |
| 51 | +== L0 — Canonical identity (THE GATE; owner decision) |
| 52 | + |
| 53 | +Resolve the *syntax schism* (ML surface for the Rust toolchain vs S-expr for the |
| 54 | +Racket core) and the *authority inversion* (docs call the 163-LOC Racket DSL |
| 55 | +"authoritative", the ~17k-LOC Rust toolchain "optional"). Recommendation, consistent |
| 56 | +with the whole architecture above: **Rust + ML surface is canonical; the Racket |
| 57 | +S-expr core becomes legacy/reference (kept, not deleted).** Fix `Justfile` / |
| 58 | +`AUTHORITY_STACK.mustfile-nickel.scm` / `CLAUDE.md` / `RSR_COMPLIANCE.adoc`. |
| 59 | + |
| 60 | +_Nothing below is well-defined until L0 is set._ Effort: *S* once decided. |
| 61 | +*Proof impact: none* (docs/config). |
| 62 | + |
| 63 | +== Core levels |
| 64 | + |
| 65 | +[cols="1,3,1,3"] |
| 66 | +|=== |
| 67 | +| Level | Goal & current state | Effort | Proof obligation |
| 68 | + |
| 69 | +| *L1 — Spec truth* |
| 70 | +| Restore/replace the missing normative `SPEC.core.scm` (referenced, absent); |
| 71 | + reconcile `spec/grammar.ebnf` with the real LALRPOP grammar so docs describe the |
| 72 | + canonical surface. The Lean small-step model *is* the semantics spine. |
| 73 | +| M |
| 74 | +| *None new.* The existing Progress/Preservation IS the normative core semantics; |
| 75 | + L1 makes the prose/grammar match it. |
| 76 | + |
| 77 | +| *L2 — Parser/AST completeness* |
| 78 | +| Verify the parser accepts the full core grammar (close any remaining gaps); |
| 79 | + AST already ~95%. |
| 80 | +| S–M |
| 81 | +| *None.* Parsing is below the Lean model (which starts from typed terms). |
| 82 | + |
| 83 | +| *L3 — Typechecker gates* |
| 84 | +| Already strong: HM + occurs-check + let-poly + `bet:Dist T` + echo. Make `check` |
| 85 | + *reject* ill-typed programs (today downgraded to warnings in `run`). |
| 86 | +| S–M |
| 87 | +| *None new* — but this is where the checker must keep matching the Lean rules |
| 88 | + (it now does for `bet:Dist T`). Keep them in lock-step. |
| 89 | + |
| 90 | +| *L4 — Interpreter runnable core* (the big one) |
| 91 | +| Today errors on 7 forms (`Do`/`Match`/`Observe`/`Infer`/`Record`/`Field`/`Index`) |
| 92 | + and starts with an EMPTY env. Bind the distribution constructors; implement the |
| 93 | + *structural* core forms (`Match`, `Record`, `Field`, `Index`, `Do`). **Design the |
| 94 | + effect-handler seam for `sample`/`observe` here** (build the metainterpreter later). |
| 95 | + Decide `Observe`/`Infer` are post-core (see §Core scope). |
| 96 | +| L |
| 97 | +| *GROWS with the language* — see §"Do we need more proofs?". Each *primitive* |
| 98 | + typed form added earns a Lean Progress/Preservation extension (the TP-5 pattern). |
| 99 | + Forms that *desugar* to the proven core need no new proof. |
| 100 | + |
| 101 | +| *L5 — Minimal program-facing stdlib* |
| 102 | +| Expose distributions, `sample`, basic list/string/math to programs on the canonical |
| 103 | + path (wire the internal `bet-rt` through; today it's only reachable via JS codegen). |
| 104 | +| M |
| 105 | +| *None new* for plain typed library functions (they instantiate existing schemes). |
| 106 | + A builtin that introduces a *new* typing/eval rule would earn a proof. |
| 107 | + |
| 108 | +| *L6 — Conformance corpus + CI gate* ← *core reached here* |
| 109 | +| Real `*.bet` fixtures in the canonical surface that parse→check→run; wire into CI |
| 110 | + as the conformance gate (today all `conformance/*.bet` are stale S-expr). |
| 111 | +| M |
| 112 | +| *None* (tests, not proofs) — but conformance is the *empirical* complement to the |
| 113 | + Lean *formal* guarantee. |
| 114 | +|=== |
| 115 | + |
| 116 | +== Core scope decision (L4) |
| 117 | + |
| 118 | +Recommended: core = deterministic + `bet`/`sample` + the structural forms |
| 119 | +(`Match`/`Do`/`Record`/`Field`/`Index`) + callable distributions + minimal stdlib. |
| 120 | +**Defer `Observe`/`Infer`** (conditioning + inference) to the post-core inference |
| 121 | +tier — they need the metainterpreter, which is a post-core build. |
| 122 | + |
| 123 | +== Design-in-now seams (the elegance/correctness investment) |
| 124 | + |
| 125 | +Owner directive (2026-06-15): defer the inference *engine*, but design its *seams* |
| 126 | +now — cheap at L4's birth, painful to retrofit, and correctness-compounding. Build |
| 127 | +only the trivial handler in core; `infer` stays post-core. |
| 128 | + |
| 129 | +. *Effect-handler seam for `sample`/`observe`.* The L4 interpreter dispatches |
| 130 | + probabilistic operations to a *handler*, not hardcoded `eval` branches. Core ships |
| 131 | + one trivial handler (`sample` = draw from RNG). The whole inference tier later is |
| 132 | + "install a different handler" (IS/MCMC/SMC) with ZERO base-interpreter change — the |
| 133 | + algebraic-effects design (cf. Gen/Pyro/Anglican). |
| 134 | +. *`Dist` as a lawful monad (`pure`/`bind`/`score`).* So `Do` *desugars* to monadic |
| 135 | + bind (no new metatheory — it's sugar over the proven core) and the already-proven |
| 136 | + *TP-3 monad laws become the runtime's semantic backbone*. |
| 137 | +. *`observe` = `score`/`factor(logpdf)`* — the measure-theoretically correct |
| 138 | + primitive. Under the default prior-sampling handler it's behaviour-preserving (so it |
| 139 | + can even run in core); `infer` is the deferred handler that *reads* the accumulated |
| 140 | + weight. Pre-pays correctness into the future *SEM-1* proof (which is provable cleanly |
| 141 | + over score semantics). |
| 142 | +. *Typed coprocessor `Handle`/`Bridge`* (`NotReady → Ready`, AffineScript pattern) in |
| 143 | + the value space now, even unused — so the eventual Axiom.jl offload plugs into a |
| 144 | + principled, typed boundary rather than an ad-hoc FFI. |
| 145 | + |
| 146 | +== Post-core tier (design seams early; build late) |
| 147 | + |
| 148 | +* *Metainterpreter = the inference engine.* For a PPL, `infer`/`observe` are |
| 149 | + implemented by intercepting `sample`/`observe` during interpretation (IS / MCMC / |
| 150 | + SMC). Plugs into the L4 effect-handler seam. (007 has a template: reify→intercept |
| 151 | + →reflect.) Also yields trace/provenance/cost for free. |
| 152 | +* *Cranelift native backend (World B).* betlang → Cranelift IR → native x86_64 |
| 153 | + (+ JIT). Cost to budget: the `bet-rt` runtime bridge (C-ABI handles + value |
| 154 | + representation across the codegen boundary). Cheaper interim native option: |
| 155 | + betlang→Rust-source→`rustc` (reuses `bet-rt` for free). |
| 156 | +* *Coprocessor acceleration (to accelerate the numeric/inference runtime, NOT the |
| 157 | + front-end).* Typed `Handle`/`Bridge` (AffineScript) → **Axiom.jl** dispatch |
| 158 | + (Julia → Zig SIMD → GPU, self-healing fallback). betlang *consumes* the estate's |
| 159 | + existing coprocessor (Axiom.jl). Caveat: Axiom.jl's GPU/coprocessor paths self-rate |
| 160 | + ~20% (need real hardware). Composition: metainterpreter = control; coprocessor = |
| 161 | + fast compute kernels. |
| 162 | +* *Grammar→parser metacompiler slice* (kills spec/impl drift; needs L1's canonical |
| 163 | + grammar first). |
| 164 | + |
| 165 | +=== Deferred proof tracks (NOT on the core path) |
| 166 | + |
| 167 | +These attach to *features*, not to the runnable core — add each when you build its |
| 168 | +feature: |
| 169 | + |
| 170 | +* *TP-5b* — richer echo surface (`echo_map`/`echo_duplicate`/`echo_to_residue`/ |
| 171 | + `sample_echo`) + comonad laws (the `MultiStep` shadow exists as reference). P3. |
| 172 | +* *SEM-1* — measure-theoretic denotation + adequacy. Needs Mathlib (architectural |
| 173 | + decision: separate Mathlib-dependent lake target vs hand-rolled). |
| 174 | +* *STAT-1 / STAT-2* — max-entropy-ternary / SLLN. Needs Mathlib. |
| 175 | +* *ABI-1..5* — Idris2 FFI proofs. P1, but only relevant once the native/FFI surface |
| 176 | + (Cranelift bridge, Julia/Axiom.jl coprocessor) exists; needs a `proof-check-idris2` |
| 177 | + recipe + CI wired first. |
| 178 | +* *CONC-1* — TLA+ parallel bet-execution. P3; subject code not ready; `tlc` absent. |
| 179 | + |
| 180 | +== Sequencing summary |
| 181 | + |
| 182 | +. *L0* (owner decision) → reframe identity. |
| 183 | +. *L1 → L2 → L3* — make the spec true, the parser complete, the checker gate. |
| 184 | +. *L4* — the runnable-core push (structural forms + callable distributions + |
| 185 | + *design* the effect-handler & coprocessor seams). Extend the Lean model for each |
| 186 | + new primitive typed form. |
| 187 | +. *L5 → L6* — minimal stdlib + conformance gate. **← core reached.** |
| 188 | +. *Post-core* — metainterpreter (inference) → Cranelift native → coprocessor offload |
| 189 | + (Axiom.jl); deferred proof tracks per feature; F# prototyping off to the side. |
| 190 | + |
| 191 | +== Proof strategy in one line |
| 192 | + |
| 193 | +The existing proofs (Progress/Preservation/type-safety/monad-laws/echo intro-elim) |
| 194 | +are *correct and sufficient for the fragment they model* and are green in CI. They |
| 195 | +are *not automatically sufficient for the larger language L4 builds*: the proof |
| 196 | +**grows with the typed core** — every new *primitive* form earns a Lean extension |
| 197 | +(TP-5 pattern), while forms that *desugar* to the proven core need none. The |
| 198 | +analytic/FFI/concurrency proofs are genuinely deferred-until-you-build-that-feature. |
| 199 | +Keep the proven core *minimal* and desugar the rest to minimise new proof debt. |
0 commit comments