hyperpolymath · hyperpolymath · Jun 22, 2026 · Jun 15, 2026
@@ -6,6 +6,15 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 This file provides context for Claude Code when working with the betlang repository.
 
+> **CANONICAL IDENTITY (owner decision, 2026-06-15 — see
+> `docs/decisions/2026-06-15-L0-canonical-identity.adoc`).** The canonical betlang
+> is the **Rust toolchain with the ML-style surface** (`compiler/*`, `runtime/*`,
+> `tools/*`) plus the Lean metatheory (`proofs/BetLang.lean`). The Racket core +
+> S-expr surface described below (`core/betlang.rkt`, `lib/`, `repl/`, `tests/`,
+> `conformance/*.bet`) is **legacy / reference — frozen, not deleted**, and is *not*
+> authoritative. Treat the "implemented in Racket" framing in this section as
+> historical; new work targets the Rust/ML surface.
+
 ## Project Overview
 
 **betlang** is a ternary DSL (Domain-Specific Language) for probabilistic modeling and symbolic wagers, implemented in Racket. The core primitive is the `(bet A B C)` form, which randomly selects one of three values, inspired by musical ternary form (A–B–A).

@@ -19,7 +19,10 @@ default:
     @just --list --unsorted
 
 # ============================================================================
-# CORE OPERATIONS (Racket - Authoritative)
+# LEGACY RACKET CORE (reference only — frozen, NOT authoritative)
+# Canonical betlang is the Rust toolchain + ML surface; see
+# docs/decisions/2026-06-15-L0-canonical-identity.adoc. These recipes drive the
+# historical Racket prototype and require `racket` (not part of the build).
 # ============================================================================
 
 # Run the betlang test suite
@@ -169,13 +172,14 @@ bench:
 status:
     @echo "=== Project Status ==="
     @echo ""
-    @echo "Authoritative implementation: Racket (core/betlang.rkt)"
-    @echo "Formal spec: SPEC.core.scm"
-    @echo "Conformance tests: conformance/"
+    @echo "Canonical implementation: Rust toolchain + ML surface (compiler/, runtime/, tools/)"
+    @echo "Mechanised metatheory: proofs/BetLang.lean (Lean 4)"
+    @echo "Legacy/reference (frozen): Racket core (core/betlang.rkt), conformance/*.bet"
+    @echo "Identity decision: docs/decisions/2026-06-15-L0-canonical-identity.adoc"
     @echo ""
     @echo "See ANCHOR.scope-arrest.2026-01-01.Jewell.scm for semantic anchor"
-    @echo "See AUTHORITY_STACK.mustfile-nickel.scm for operational authority"
-    @echo "See TOOLING.md for optional tooling documentation"
+    @echo "See AUTHORITY_STACK.mustfile-nickel.scm for operational authority (just/must)"
+    @echo "See docs/decisions/2026-06-15-betlang-core-plan.adoc for the core build plan"
 
 # ============================================================================
 # CLEAN

@@ -15,10 +15,10 @@ This document describes the Rhodium Standard Repository (RSR) compliance status
 |Attribute |Value
 
 |Project |betlang
-|Primary Language |unknown
-|RSR Tier |N/A
-|Compliance Status |Review Needed
-|Last Updated |2025-12-10
+|Primary Language |Rust (canonical toolchain — see docs/decisions/2026-06-15-L0-canonical-identity.adoc)
+|RSR Tier |Tier 1 (Rust)
+|Compliance Status |Active — core build in progress
+|Last Updated |2026-06-15
 |===
 
 == Language Tier Classification
@@ -48,7 +48,7 @@ This document describes the Rhodium Standard Repository (RSR) compliance status
 |===
 |Requirement |Status |Notes
 
-|Primary language is Tier 1/2 |✓ |unknown
+|Primary language is Tier 1/2 |✓ |Rust (Tier 1)
 |No restricted languages outside exemptions |✓ |
 |.editorconfig present |✓ |
 |.well-known/ directory |✓ |

@@ -0,0 +1,43 @@
+// SPDX-License-Identifier: MPL-2.0
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+= L0 — Canonical identity of betlang
+:toc:
+
+Status: *DECIDED (owner, 2026-06-15)*. Gate for the core build plan
+(link:2026-06-15-betlang-core-plan.adoc[]).
+
+== Decision
+
+The *canonical betlang* is the **Rust toolchain with the ML-style surface syntax**:
+`compiler/*` (bet-syntax/parse/core/check/eval/codegen/wasm), `runtime/*`
+(bet-rt/bet-rand/bet-viz), `tools/*` (bet-cli/bet-lsp/bet-dap), and the mechanised
+Lean metatheory at `proofs/BetLang.lean`. All future language work (spec, grammar,
+typechecker, interpreter, stdlib, conformance) targets this surface.
+
+The **Racket core + S-expr surface** (`core/betlang.rkt`, `lib/`, `repl/shell.rkt`,
+`tests/basics.rkt`, and the `conformance/*.bet` S-expr corpus) is reclassified as
+**legacy / reference — frozen, NOT deleted**. It remains as historical record and an
+executable second opinion; it is not built upon and is not authoritative.
+
+== Why
+
+* The Rust toolchain holds ~17k LOC of real machinery; the Lean proof models the
+  ML/Rust core; the entire 2026-06-15 architecture pass (bet:Dist T, the unified
+  `bet_rt::Value` runtime, World-B native/Cranelift, the inference seams) lives there.
+* The prior "Racket is authoritative / Rust is optional" framing was an *authority
+  inversion* — the documented authority pointed at a 163-LOC prototype while the real
+  language lived in the "optional" toolchain. This decision corrects that.
+* `racket` is not part of the build/runtime; keeping it authoritative blocked a
+  coherent core.
+
+== Consequences
+
+* Docs reframed to match: `CLAUDE.md`, `Justfile` (CORE OPERATIONS header + `status`
+  recipe), `RSR_COMPLIANCE.adoc` (Primary Language → Rust, Tier 1).
+* `AUTHORITY_STACK.mustfile-nickel.scm` is unchanged — it governs the *operational
+  interface* (just/must/nickel/podman), which is language-agnostic and still holds.
+* L6 will rebuild the conformance corpus in the ML surface; the S-expr corpus stays
+  as frozen reference.
+* The Racket side is *frozen, not removed* (per the estate "never delete by
+  access-recency / foundational work is cold" rule).
@@ -0,0 +1,199 @@
+// SPDX-License-Identifier: MPL-2.0
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+= betlang — Core Build Plan (core → post-core tier)
+:toc:
+:sectnums:
+
+The level-by-level plan to bring betlang to *absolutely core* — a single-identity
+language that **runs real probabilistic programs end to end** — followed by the
+post-core tier (native compile + inference + coprocessor acceleration). Companion
+to link:2026-06-15-betlang-wiring-and-bet-dist-t.adoc[the wiring/bet:Dist T ADR log].
+
+== Definition of "absolutely core"
+
+____
+You write a real betlang program in ONE canonical syntax, and `bet check` +
+`bet run` parse it, type-check it (`bet : Dist T`), and **interpret it correctly
+end to end** — distributions and a minimal stdlib are callable, type errors are
+real errors, and a conformance corpus in that syntax is green in CI. The Lean
+proof certifies the typed core on top of that.
+____
+
+Everything else — extra backends, native compile, full PPL inference, the meta
+layer, Julia/aLib/StatistEase, the analytic/FFI/concurrency proofs — is *post-core*.
+
+== Locked architecture decisions (from the 2026-06-15 design pass)
+
+* *One production language: Rust.* Front-end (parse/check/AST), interpreter, the
+  `bet-rt` runtime, and the eventual native backend are all Rust. No polyglot
+  production pipeline (avoids a cross-language seam / interstitial drift).
+* *Two execution tiers.* **Iterate** = tree-walking interpreter (core). **Deploy**
+  = compile (post-core). Don't put a compiler on the iterate path.
+* *World B (native).* Native x86_64 via **Cranelift** (pure-Rust, fast, JIT-capable);
+  inference offloaded to **Julia (Turing.jl) + Axiom.jl**; *not* .NET. (Rejected:
+  betlang→.NET/Infer.NET — would be a second runtime; .NET's own JIT makes Cranelift
+  redundant in that world. Rejected: F# as a production stage — second runtime,
+  can't share `bet-rt` or feed Cranelift.)
+* *F# = optional prototyping/reference lane, off the shipped path.* Use `dotnet fsi`
+  to sketch a new semantics, then port the settled design to Rust. Never shipped.
+  (The estate's sanctioned ML-compiler lane is OCaml; the Lean model + legacy Racket
+  core already partly occupy the "reference oracle" niche.)
+* *Two seams: design EARLY, build LATE.*
+  ** an *effect-handler seam* for `sample`/`observe` in the interpreter — this is
+     what a metainterpreter (= the inference engine) plugs into;
+  ** a *typed coprocessor `Handle`/`Bridge`* (AffineScript pattern: `NotReady →
+     Ready(Bridge)`) routing numeric kernels to **Axiom.jl** (Julia → Zig SIMD →
+     GPU, self-healing fallback).
+* *Metacompiler:* only the *grammar → parser generation* slice is in scope (post-L1,
+  to kill spec/impl drift). Full staging / partial-evaluation is deferred.
+
+== L0 — Canonical identity (THE GATE; owner decision)
+
+Resolve the *syntax schism* (ML surface for the Rust toolchain vs S-expr for the
+Racket core) and the *authority inversion* (docs call the 163-LOC Racket DSL
+"authoritative", the ~17k-LOC Rust toolchain "optional"). Recommendation, consistent
+with the whole architecture above: **Rust + ML surface is canonical; the Racket
+S-expr core becomes legacy/reference (kept, not deleted).** Fix `Justfile` /
+`AUTHORITY_STACK.mustfile-nickel.scm` / `CLAUDE.md` / `RSR_COMPLIANCE.adoc`.
+
+_Nothing below is well-defined until L0 is set._ Effort: *S* once decided.
+*Proof impact: none* (docs/config).
+
+== Core levels
+
+[cols="1,3,1,3"]
+|===
+| Level | Goal & current state | Effort | Proof obligation
+
+| *L1 — Spec truth*
+| Restore/replace the missing normative `SPEC.core.scm` (referenced, absent);
+  reconcile `spec/grammar.ebnf` with the real LALRPOP grammar so docs describe the
+  canonical surface. The Lean small-step model *is* the semantics spine.
+| M
+| *None new.* The existing Progress/Preservation IS the normative core semantics;
+  L1 makes the prose/grammar match it.
+
+| *L2 — Parser/AST completeness*
+| Verify the parser accepts the full core grammar (close any remaining gaps);
+  AST already ~95%.
+| S–M
+| *None.* Parsing is below the Lean model (which starts from typed terms).
+
+| *L3 — Typechecker gates*
+| Already strong: HM + occurs-check + let-poly + `bet:Dist T` + echo. Make `check`
+  *reject* ill-typed programs (today downgraded to warnings in `run`).
+| S–M
+| *None new* — but this is where the checker must keep matching the Lean rules
+  (it now does for `bet:Dist T`). Keep them in lock-step.
+
+| *L4 — Interpreter runnable core* (the big one)
+| Today errors on 7 forms (`Do`/`Match`/`Observe`/`Infer`/`Record`/`Field`/`Index`)
+  and starts with an EMPTY env. Bind the distribution constructors; implement the
+  *structural* core forms (`Match`, `Record`, `Field`, `Index`, `Do`). **Design the
+  effect-handler seam for `sample`/`observe` here** (build the metainterpreter later).
+  Decide `Observe`/`Infer` are post-core (see §Core scope).
+| L
+| *GROWS with the language* — see §"Do we need more proofs?". Each *primitive*
+  typed form added earns a Lean Progress/Preservation extension (the TP-5 pattern).
+  Forms that *desugar* to the proven core need no new proof.
+
+| *L5 — Minimal program-facing stdlib*
+| Expose distributions, `sample`, basic list/string/math to programs on the canonical
+  path (wire the internal `bet-rt` through; today it's only reachable via JS codegen).
+| M
+| *None new* for plain typed library functions (they instantiate existing schemes).
+  A builtin that introduces a *new* typing/eval rule would earn a proof.
+
+| *L6 — Conformance corpus + CI gate* ← *core reached here*
+| Real `*.bet` fixtures in the canonical surface that parse→check→run; wire into CI
+  as the conformance gate (today all `conformance/*.bet` are stale S-expr).
+| M
+| *None* (tests, not proofs) — but conformance is the *empirical* complement to the
+  Lean *formal* guarantee.
+|===
+
+== Core scope decision (L4)
+
+Recommended: core = deterministic + `bet`/`sample` + the structural forms
+(`Match`/`Do`/`Record`/`Field`/`Index`) + callable distributions + minimal stdlib.
+**Defer `Observe`/`Infer`** (conditioning + inference) to the post-core inference
+tier — they need the metainterpreter, which is a post-core build.
+
+== Design-in-now seams (the elegance/correctness investment)
+
+Owner directive (2026-06-15): defer the inference *engine*, but design its *seams*
+now — cheap at L4's birth, painful to retrofit, and correctness-compounding. Build
+only the trivial handler in core; `infer` stays post-core.
+
+. *Effect-handler seam for `sample`/`observe`.* The L4 interpreter dispatches
+  probabilistic operations to a *handler*, not hardcoded `eval` branches. Core ships
+  one trivial handler (`sample` = draw from RNG). The whole inference tier later is
+  "install a different handler" (IS/MCMC/SMC) with ZERO base-interpreter change — the
+  algebraic-effects design (cf. Gen/Pyro/Anglican).
+. *`Dist` as a lawful monad (`pure`/`bind`/`score`).* So `Do` *desugars* to monadic
+  bind (no new metatheory — it's sugar over the proven core) and the already-proven
+  *TP-3 monad laws become the runtime's semantic backbone*.
+. *`observe` = `score`/`factor(logpdf)`* — the measure-theoretically correct
+  primitive. Under the default prior-sampling handler it's behaviour-preserving (so it
+  can even run in core); `infer` is the deferred handler that *reads* the accumulated
+  weight. Pre-pays correctness into the future *SEM-1* proof (which is provable cleanly
+  over score semantics).
+. *Typed coprocessor `Handle`/`Bridge`* (`NotReady → Ready`, AffineScript pattern) in
+  the value space now, even unused — so the eventual Axiom.jl offload plugs into a
+  principled, typed boundary rather than an ad-hoc FFI.
+
+== Post-core tier (design seams early; build late)
+
+* *Metainterpreter = the inference engine.* For a PPL, `infer`/`observe` are
+  implemented by intercepting `sample`/`observe` during interpretation (IS / MCMC /
+  SMC). Plugs into the L4 effect-handler seam. (007 has a template: reify→intercept
+  →reflect.) Also yields trace/provenance/cost for free.
+* *Cranelift native backend (World B).* betlang → Cranelift IR → native x86_64
+  (+ JIT). Cost to budget: the `bet-rt` runtime bridge (C-ABI handles + value
+  representation across the codegen boundary). Cheaper interim native option:
+  betlang→Rust-source→`rustc` (reuses `bet-rt` for free).
+* *Coprocessor acceleration (to accelerate the numeric/inference runtime, NOT the
+  front-end).* Typed `Handle`/`Bridge` (AffineScript) → **Axiom.jl** dispatch
+  (Julia → Zig SIMD → GPU, self-healing fallback). betlang *consumes* the estate's
+  existing coprocessor (Axiom.jl). Caveat: Axiom.jl's GPU/coprocessor paths self-rate
+  ~20% (need real hardware). Composition: metainterpreter = control; coprocessor =
+  fast compute kernels.
+* *Grammar→parser metacompiler slice* (kills spec/impl drift; needs L1's canonical
+  grammar first).
+
+=== Deferred proof tracks (NOT on the core path)
+
+These attach to *features*, not to the runnable core — add each when you build its
+feature:
+
+* *TP-5b* — richer echo surface (`echo_map`/`echo_duplicate`/`echo_to_residue`/
+  `sample_echo`) + comonad laws (the `MultiStep` shadow exists as reference). P3.
+* *SEM-1* — measure-theoretic denotation + adequacy. Needs Mathlib (architectural
+  decision: separate Mathlib-dependent lake target vs hand-rolled).
+* *STAT-1 / STAT-2* — max-entropy-ternary / SLLN. Needs Mathlib.
+* *ABI-1..5* — Idris2 FFI proofs. P1, but only relevant once the native/FFI surface
+  (Cranelift bridge, Julia/Axiom.jl coprocessor) exists; needs a `proof-check-idris2`
+  recipe + CI wired first.
+* *CONC-1* — TLA+ parallel bet-execution. P3; subject code not ready; `tlc` absent.
+
+== Sequencing summary
+
+. *L0* (owner decision) → reframe identity.
+. *L1 → L2 → L3* — make the spec true, the parser complete, the checker gate.
+. *L4* — the runnable-core push (structural forms + callable distributions +
+  *design* the effect-handler & coprocessor seams). Extend the Lean model for each
+  new primitive typed form.
+. *L5 → L6* — minimal stdlib + conformance gate. **← core reached.**
+. *Post-core* — metainterpreter (inference) → Cranelift native → coprocessor offload
+  (Axiom.jl); deferred proof tracks per feature; F# prototyping off to the side.
+
+== Proof strategy in one line
+
+The existing proofs (Progress/Preservation/type-safety/monad-laws/echo intro-elim)
+are *correct and sufficient for the fragment they model* and are green in CI. They
+are *not automatically sufficient for the larger language L4 builds*: the proof
+**grows with the typed core** — every new *primitive* form earns a Lean extension
+(TP-5 pattern), while forms that *desugar* to the proven core need none. The
+analytic/FFI/concurrency proofs are genuinely deferred-until-you-build-that-feature.
+Keep the proven core *minimal* and desugar the rest to minimise new proof debt.