Registry surfaces reconciled 2026-07-02; language grades below unverified since 2026-03-21.
This coordinator tracks the language family, the KitchenSpeak DSL and Firmboot’s
continuity research prototype, each maintained as its own standalone repo (no
language code lives here). In the existing integration record, 11 languages are
registered in the BoJ Server lang-mcp cartridge (plus one retired slot, ID 11 — see
below) with session management, type-checking, and evaluation via zig adapter + Zig FFI.
Adjacent database / type-theory estates are listed separately at the end of this section
and are out of coordinator scope.
Per-language grades against the five hyperpolymath language-grade standards:
-
CRG (Component Readiness Grades) — worst-of any released component
-
TRG (Toolchain Readiness Grades) — language toolchain (parser, type checker, codegen…)
-
ARG (Adoption Readiness Grades) — language as adoptable artefact
-
FRG (Foundations Readiness Grades) — mathematical foundations
-
RSR (Rhodium Standard Repositories) — repository hygiene compliance level
All graders use X | F | E | D | C | B | A. The grade source of truth lives in each
language’s repo at spec/{ARG,FRG,TRG}-PROFILE.adoc; the values below are mirrored
here for at-a-glance comparison and are cross-checked against language-status-tracker.jl
output (that script reports; it does not rewrite this file).
Cross-axis invariants: ARG ≤ TRG always; ARG-A requires FRG ≥ B.
| Language | CRG | TRG | ARG | FRG | RSR | Notes |
|---|---|---|---|---|---|---|
AffineScript |
TBD |
TBD |
D |
E |
FULL |
ARG-D leaning; CLI gates programs. FRG-E pragmatic / X strict (no |
Ephapax |
TBD |
TBD |
E |
D |
FULL |
Strong FRG narrative (preservation stated, layered redesign committed). Adoption surface sparse. |
My |
TBD |
TBD |
D-leaning-E |
X |
FULL |
11 crates, 3 dialects (Solo ⊂ Duet ⊂ Ensemble; Me is a runtime projection, not a dialect). PROOF-NEEDS.md honestly records template-ABI removal (FRG-X discipline). |
Eclexia |
TBD |
TBD |
TBD |
TBD |
TBD |
Profile not yet authored. |
Betlang |
TBD |
TBD |
TBD |
TBD |
TBD |
Profile not yet authored. |
Phronesis |
TBD |
TBD |
TBD |
TBD |
TBD |
Profile not yet authored. |
Wokelang |
TBD |
TBD |
TBD |
TBD |
TBD |
Profile not yet authored. |
Anvomidav |
TBD |
TBD |
TBD |
TBD |
TBD |
Profile not yet authored. |
JtV |
TBD |
TBD |
TBD |
TBD |
TBD |
Profile not yet authored. |
Oblibeny |
TBD |
TBD |
TBD |
TBD |
TBD |
Profile not yet authored. |
Error-lang |
TBD |
TBD |
TBD |
TBD |
TBD |
Profile not yet authored. |
Haec |
TBD |
TBD |
TBD |
TBD |
FULL |
Trope-particularity front-end (design pass: grammar + elaboration + round-tripping examples). Siblings: trope-checker (Idris2 verified core + executable checker, conformance), trope-particularity-workbench (the nine-effect vocabulary). |
Kitchenspeak |
TBD |
TBD |
TBD |
TBD |
TBD |
Proofs commenced (Dough, PoachedEgg, EchoBridge); ADR 0001–0004; echo-types dependency. Profile not yet authored. |
Tangle |
TBD |
TBD |
TBD |
TBD |
TBD |
Topological (knot/braid) language; Lean core proofs. TangleIR feeds the separate KRL resolution stack (see Adjacent estates). |
007 |
TBD |
TBD |
TBD |
TBD |
TBD |
Agent meta-language; private repo ( |
Firmboot |
TBD |
TBD |
TBD |
TBD |
TBD |
Research prototype: checked Agda/Lean models and Elixir reference runner. See evidence and limits. No readiness grade or BoJ integration is claimed. |
Me-dialect (retired) |
X |
X |
X |
X |
X |
RETIRED — superseded by the Me runtime projection ( |
Tracked by the database / type-theory estates, listed here only for discoverability — they
are not part of the language family and are not registered in .machine_readable/LANGUAGES.a2ml:
-
VCL-total (vcl-ut) — database/identity language; per ARG §1.1 tightening applies.
-
KRL — resolution language at the base of the KRL stack (
krl → Tangle/TangleIR → VeriSimCore → Skein.jl / quandledb); distinct from the Tangle language above, whose IR it consumes. Canonical READINESS.md template lives there. -
Quandledb — database language.
-
TypeLL — type-theory foundation, feeds VCL-total levels.
-
PanLL — type-theory foundation.
Standards specs:
-
standards/component-readiness-grades/ -
standards/toolchain-readiness-grades/ -
standards/adoption-readiness-grades/ -
standards/foundations-readiness-grades/ -
standards/rhodium-standard-repositories/
| Language | Compiler | LSP | DAP | Linter | Formatter | Tree-sitter | Doc Gen | Pkg Mgr | Conformance |
|---|---|---|---|---|---|---|---|---|---|
Eclexia |
25 crates (Rust) |
eclexia-lsp |
eclexia-dap |
eclexia-lint |
eclexia-fmt |
— |
eclexia-doc |
— |
✓ + fuzz |
Betlang |
7 crates (Rust) |
bet-lsp (Gleam) |
bet-dap |
— |
— |
— (LALRPOP) |
— |
— |
✓ + fuzz |
AffineScript |
OCaml |
affine-lsp (Rust) |
affine-dap (Rust) |
linter.ml |
stub |
tree-sitter |
affine-doc |
affine-pkg |
✓ |
Ephapax |
Idris2-based |
planned |
planned |
— |
— |
— |
— |
— |
— |
Wokelang |
Rust |
planned |
planned |
— |
— |
— |
— |
— |
✓ |
My-Lang |
7 components |
✓ |
planned |
— |
— |
— |
— |
— |
— |
JtV |
Idris2 ABI |
planned |
planned |
— |
— |
— |
— |
— |
✓ + benchmarks |
Tangle |
Rust |
tangle-lsp |
planned |
— |
— |
— (EBNF) |
— |
— |
— |
Phronesis |
Rust |
planned |
planned |
— |
— |
— (tmLanguage) |
— |
— |
✓ |
Oblibeny |
OCaml |
✓ |
✓ |
— |
— |
— |
— |
— |
— |
Error-lang |
Rust |
error-lang-lsp |
planned |
— |
— |
— (tmLanguage) |
— |
— |
✓ |
Me-dialect (retired) |
— |
— |
— |
— |
— |
— |
— |
— |
— (superseded by the Me projection — tentacles-agentic-syllabus/me) |
12 lang-mcp IDs exist in boj-server/cartridges/lang-mcp/ — 11 active languages plus the
retired Me-dialect slot (ID 11, kept because IDs are positional):
| Language | ID | BoJ Features |
|---|---|---|
Eclexia |
1 |
Session, typecheck, eval, compile |
AffineScript |
2 |
Session, typecheck, eval, compile |
Betlang |
3 |
Session, typecheck, eval, compile |
Ephapax |
4 |
Session, typecheck, eval, compile |
My-Lang |
5 |
Session, typecheck, eval, compile |
Wokelang |
6 |
Session, typecheck, eval, compile |
Anvomidav |
7 |
Session (stub) |
Phronesis |
8 |
Session, typecheck, eval |
Error-lang |
9 |
Session, typecheck, eval |
JtV |
10 |
Session, typecheck, eval, dialect injection |
Me-dialect (retired) |
11 |
Slot retained (IDs are positional); superseded by the Me projection — do not register new work here |
Oblibeny |
12 |
Session, typecheck, eval |
-
lang-mcp — Language sessions (zig adapter, Zig FFI, PanLL panels)
-
lsp-mcp — Generic LSP proxy (ABI/FFI/adapter/panels)
-
dap-mcp — Generic DAP proxy (ABI/FFI/adapter/panels)
| Language | Idris2 ABI | Zig FFI | Status |
|---|---|---|---|
AffineScript |
|
planned |
In progress |
JtV |
|
planned |
In progress |
Ephapax |
ephapax-proven (3 crates) |
proven-ffi |
Complete |
Others |
— |
— |
Not started |
-
Ephapax — Linear type proofs via Idris2
-
AffineScript — Affine type proofs (linear subset)
-
Eclexia — Effect system proofs (
eclexia-effectscrate)