nextgen-languages is a pure coordinator and holds no proof code.
This file tracks the family’s proof gaps across the standalone
hyperpolymath/<lang> repos; every path below is relative to the
named language’s own repo, not this one.
-
Ephapax — Coq proofs present; 4
Admittedremain informal/Semantics.v(ctx_transfer 15/24, subst_lemma, preservation,
one more). -
Tangle — Lean proofs present (
Tangle.lean); coverage partial. -
Oblíbený — Idris2 ABI present (
src/abi/Interface.idr); minimal. -
AffineScript — OCaml type checker + Rust runtime; soundness proofs outstanding.
| Component | What | Why |
|---|---|---|
Ephapax ctx_transfer (15/24 cases) |
Close remaining 9 context transfer cases in Semantics.v |
Core type safety theorem is incomplete |
Ephapax subst_lemma |
Prove substitution lemma |
Required for preservation theorem |
Ephapax preservation |
Close preservation theorem (depends on subst_lemma) |
Type preservation is THE fundamental safety property |
Ephapax 4th Admitted |
Close the 4th Admitted in Semantics.v |
Blocks full formal verification claim |
AffineScript type safety |
Prove OCaml type checker is sound |
AffineScript claims affine types but lacks proofs |
AffineScript runtime (Rust) |
GC and allocator correctness |
Memory safety of the runtime is critical |
Betlang type checker |
Prove bet-check is sound |
Compiler correctness depends on type checking |
Tangle Lean proofs |
Extend Tangle.lean coverage |
Existing Lean proofs are partial |
Oblibeny ABI |
Extend Interface.idr with full package proofs |
Current ABI is minimal |
KitchenSpeak is now an external standalone repo; its Agda proofs and
their trusted base (postulated echo-oracles / sensors and the GENTLE
controller spec) live in hyperpolymath/kitchenspeak, not in this
coordinator.
Coq for Ephapax (existing proof infrastructure). Lean4 for Tangle (existing). Idris2 for ABI layers. OCaml extraction from Coq for AffineScript type checker verification.