-
-
Notifications
You must be signed in to change notification settings - Fork 0
Home
A research programming language with a mechanised metatheory: an affine / Quantitative-Type-Theory core whose soundness is proved on two independent tracks — Coq/Rocq (authoritative) and Idris2 (twin) — with the verified usage-checker ported into the Rust compiler.
my-lang is a sibling of AffineScript, not a fork.
Status:
0.2.0— early alpha, experimental. No tagged release. 221 tests pass (0 failures, measured 2026-08-07).
Every binder carries a usage quantity from the QTT semiring {0, 1, ω}
— erased, linear, or unrestricted — and the theorems that make that discipline
sound are machine-checked, axiom-free, and re-checked by CI on every change to
the proof tree.
| Proved twice | The solo core is mechanised in Coq and Idris2. The Coq track is authoritative; progress, preservation and affine_pres are real Qed. with Print Assumptions reporting "Closed under the global context" — asserted in CI, per rung. |
| Parametric soundness | The Coq core is a functor SoloCoreF (M : ORDERED_SEMIRING). Soundness is proved over the resource algebra, so instantiating at Linear3 recovers the concrete language and at Tropical (min-plus, infinite carrier) it still holds axiom-free — with no new proof. |
| Proof→implementation coupling | The Coq check function is an executable verified spec with check_correct : has_type G D t a ↔ check G t = Some (a, D), hand-ported into the my-qtt crate. Closing the gap between that spec and the Rust checker is the project's headline goal. |
| Echo types |
Echo<A => B> — a proof-relevant residue of a lossy collapse. Deliberately narrow: a loss-graded reindexing modality over a thin poset, not a graded comonad. |
| Session-typed concurrency, as metatheory | A standalone Coq development proves subject reduction, session fidelity, and deadlock-freedom for the binary fragment, plus duet-by-projection and n-party projection totality. |
| Honesty as infrastructure | A precise status vocabulary (machine-checked / locally-checked / proved-on-paper / statement-only / definitions-only / absent) and the standing rule: no proof hole is ever described as proved. |
Dialects are nested conservative extensions, not four peers:
Solo ⊂ Duet ⊂ Ensemble (+ me — a projection, not a compiler)
Only Solo is authoritative in f0, per the repository's scope-arrest
anchor. Duet and Ensemble exist as proof developments plus scaffolding — not as
usable compilers. me is an on-the-fly, agent-generated projection over
the hierarchy, with a machine-checked me → solo elaboration-correctness
theorem (me_wt_sound).
- Getting Started — the only install path that works today
- Architecture — crates, pipeline, and where the real code lives
- Formal Verification — what is actually proved, and what isn't
- Project Status — measured state and known debt
This wiki is a navigational layer. It is deliberately thin and links to documents inside the repository, which are the ones kept in step with the code — so this wiki cannot quietly drift out of date.
The fuller prose documentation lives in
docs/wiki/.
Be aware that several pages there describe intended rather than implemented
behaviour; those carry an explicit warning banner, and the gaps are catalogued
in DEBT.md.
MPL-2.0 for code, CC-BY-SA-4.0 for documentation.