my-lang

Important

README.md is the canonical README for this repository. This AsciiDoc file is retained because estate tooling references it. It is a short summary only — for the full picture (proof-status table, repository map, golden path, security posture) read README.md. An earlier, much longer version of this file drifted badly out of date and contradicted README.md on test counts, proof phase, dialect structure and directory layout. It was replaced on 2026-08-07 rather than left to mislead.

What this is

my-lang is a research programming language with a mechanised metatheory: an affine / Quantitative-Type-Theory (QTT {0, 1, ω}) 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.

It is a sibling of AffineScript, not a fork.

Dialects

The dialects are nested conservative extensions, not four peers:

Solo ⊂ Duet ⊂ Ensemble        (+ me, a projection — not a fourth compiler)

Only Solo is authoritative in f0, per the scope-arrest anchor (ANCHOR.scope-arrest.2026-01-01.Jewell.scm). Duet and Ensemble exist as proof developments and scaffolding; me is an on-the-fly, agent-generated projection over the hierarchy with a machine-checked me → solo elaboration-correctness theorem.

Status

• Version: 0.2.0 — early alpha, experimental. No tagged release.

• Licence: MPL-2.0 (code), CC-BY-SA-4.0 (documentation). Migrated from PMPL-1.0-or-later on 2026-05-26; see PALIMPSEST.adoc.

• Tests: 221 pass, 0 failures (just test, excludes my-llvm).

• Proofs: proofs/STATUS.md is the single authoritative registry. Progress, preservation and affine_pres are machine-checked and axiom-free on the Coq track, CI-gated per rung.

Key documents

File	Purpose
README.md	Canonical README
EXPLAINME.adoc	Gentle conceptual orientation
ARCHITECTURE.md	Structure and dialect containment
ROADMAP.adoc	What is done, next, and explicitly not planned
DEBT.md	Known licence / docs / code / proof / CI debt
proofs/STATUS.md	Authoritative proof-status registry
.machine_readable/6a2/STATE.a2ml	Authoritative machine-readable state

Golden path

just init     # submodules
just check    # fmt-check + lint + test
just proofs   # both proof tracks