README.md

my-lang

my-lang is the next-generation language working project — a multi-dialect surface for the hyperpolymath language stack. It is one of two flagship language experiments in the estate (the other being affinescript). The two projects are siblings, not a fork — they share design principles but diverge in dialect scope and proof strategy.

For a gentler entry point see EXPLAINME.adoc.

What's in here

Path	Contents
crates/	Rust compiler crates. crates/my-lang/src/types.rs is the type checker, including EchoMode, Ty::Echo, and full affine-weakening semantics.
dialects/	Per-dialect surface-syntax definitions: solo (affine, single-agent), duet (session-typed), ensemble (multi-agent), me (visual/pedagogic).
proofs/	Formal verification assets — paper proofs, mechanised Coq + Idris2 solo-core. See proofs/STATUS.md for the authoritative proof-status registry.
conformance/	Conformance tests — programs any compliant implementation must accept or reject identically.
examples/	Worked examples for each dialect.
docs/	Design notes, ADRs. Includes the echo-types integration design note.
frontier-practices/	Forward-looking research experiments (not shipped).
contractiles/	Project-level Mustfile / Dustfile invariant and recovery contracts.

Quickstart

git clone git@github.com:hyperpolymath/my-lang.git
cd my-lang

just build    # builds the workspace (Rust)
just test     # runs unit + conformance tests

To check the Coq solo-core:

cd proofs/verification/coq/solo-core
coq_makefile -f _CoqProject -o CoqMakefile && make -f CoqMakefile

To check the Idris2 solo-core:

cd proofs/verification/idris/solo-core
idris2 --build solo-core.ipkg

Proof and verification status

my-lang follows a statements-first, machine-checked later proof methodology mirroring affinescript's solo-core approach. proofs/STATUS.md is the single authoritative source — no proof is described as "proved" there until a proof assistant accepts it.

Current state (2026-06-13):

Artefact	Status
QTT semiring + laws (Coq + Idris2)	machine-checked — all laws proved by exhaustive case analysis; run in CI (proofs.yml)
Solo syntax, contexts, typing (Coq + Idris2)	locally-checked
Operational semantics (CBV small-step)	locally-checked — Phase F1.1 done (both tracks)
Progress	machine-checked (Coq) — Phase F1.3 done: Coq Theorem progress : Progress. real Qed. (axiom-free), CI-guarded (proofs.yml); Idris progress hole-free/total (only preservation carries a ?todo)
Preservation	machine-checked (Coq) — Phase F1.4 done on the Coq track: Theorem preservation : Preservation. and affine_pres are real Qed. (axiom-free, Print Assumptions closed), via the open-context QTT substitution lemma ht_subst. Product/elimination decision settled (additive & + multiplicative ⊗ both coherent). Idris twin pending (Phase F5 parity).
Usage-walk checker (check)	machine-checked (Coq) — Phase F1.4 tail / R5 done: check : tctx → tm → option (ty × uvec) synthesises type and usage in one bottom-up pass, with check_correct : has_type G D t a ↔ check G t = Some (a, D) a real Qed. (axiom-free, CI-guarded). This is the decidability/adequacy of QTT typing — the executable spec the Rust dialects/solo checker (still TODO(#typeck)) must meet, and it overtakes AffineScript (whose solo-core leaves the same equivalence as prose "future work"). R5b further decides the affine budget judgement (aff_type_dec).
me → solo elaboration (elab, elab_data_check, me_wt_sound)	machine-checked (Coq) — M1.0 / M1.1 / M1.1b done: the visual me surface (proofs/me/) elaborates into the solo core. elab : me_tm → tm is a core-landing analogue of the paper translate. M1.1 elab_data_check is the axiom-free Visual-Soundness theorem for the no-linear-use data fragment; M1.1b adds a me typing judgement me_wt with me_wt_sound : me_wt G D e a → has_type G D (elab e) a covering the linear-use constructs (token-consume / MeLet / pair-split / the faithful MeIf → Case conditional) universally — spanning the whole me_tm (incl. MeSeq, closed via the F1.4 ht_shift0 weakening lemma). The first mechanised surface→core elaboration-correctness result in either sibling — AffineScript, as surveyed (proofs/ALIGNMENT-PLAN.md §1, AS@main 2026-06-02), is solo-only with no me-like dialect.
Ensemble session-π core (SessionPi.v: proc, sty/dual, wt, step)	machine-checked (Coq), definitions + witnesses — S1.0 done (axis-2 STRUCTURE): a standalone Coq development for the ensemble session-typed π-calculus (binary, synchronous) after proofs/duet/session-types/ + proofs/ensemble/agent-calculus/. Session types with a computed duality + dual_involutive, polarised endpoints, a linear channel-typing judgement with context splitting, and small-step reduction for the communication redex; executable witnesses (a well-typed ping-pong that reduces) are real Qed, axiom-free and CI-guarded. S1.1a/S1.1b done: the first-order value-substitution lemma (wt_subst) and subject reduction for the communication redex (sr_comm) are real axiom-free Qed; and full closed-system subject reduction (config_subject_reduction : wf_config c → cstep c c' → wf_config c') is proved axiom-free via the fused two-party (νc)(P∣Q) form (the duet T-Session primitive), where the shared protocol advances locally so well-formedness (both endpoints dual) is preserved across communication. S1.2 done: session fidelity (session_fidelity — a communication advances the protocol by exactly one sty_step) and progress / deadlock-freedom (config_progress — a well-formed config is fully ended or can step), the duet paper's safety+liveness theorems for the binary fragment, both axiom-free. S2.0/S2.1 done — duet by projection: a multiparty-shaped global-type layer gty + the three-case projection proj G r (sender ! / receiver ? / uninvolved passthrough) + the two-party restriction two_party, with projection_duality (a two-party choreography projects to DUAL local types — p≠q load-bearing) and projected_config_wf + corollaries that transport the whole S1.1b/S1.2 guarantee across projection (subject reduction, fidelity, progress) — so a config obtained by projecting a choreography is deadlock-free BY CONSTRUCTION, all axiom-free. Honest fence: message-passing + end only; it instantiates the thesis on two-party choreographies (not a general n-party result); choice/μ landed at S2.2 (below) and n≥3 coherence (S3) is OUT. S1.3 done — choice / congruence / μ type-layer: S1.3a extends the three fused theorems with n-ary labelled choice (SSelect/SBranch/QSel/QBra over dedicated mutual inductives, label-mismatch safety expressible); S1.3c proves structural congruence preserves typing on the open proc (wt_congr, par laws); S1.3b-core adds the equi-recursive μ type-layer (SMu/SVar, unfold_mu, dual_unfold, guarded) — the S2.2 projection target — all axiom-free. (μ typing/SR up-to-unfolding = S1.3b-meta, honestly deferred.) S2.2 done — choice + recursion by projection: global types gain labelled choice GBra p→q:{lᵢ:Gᵢ} + equi-recursive GMu/GVar; projection becomes partial (proj : gty → role → option sty, three-way mutual) with a plain merge (keystone merge_idem) combining the branches for an uninvolved role, and projection_duality is reproved in option-map form over choice + μ (mutual two_party_mut scheme), the whole bridge rethreaded through proj … = Some _. Design-panel-validated (caught a real None-erasure soundness bug pre-implementation). Honest fences: plain (not label-union) merge, unpruned μ projection, no global-level metatheory; full-union merge + n-party safety = S3c. S3a done — n-party projection totality: the first theorem quantifying over a genuine n≥3 role space, projection_total : projectable_wf G → ∀ r:role, ∃ s, proj G r = Some s (every role of a well-branched global type projects), via the mutual projectable_wf_mut scheme; non-vacuity pinned at n=3 by a 3-party ring (projects on all roles, not two_party) and an agreeing 3-party choice (uninvolved role projected via a non-trivial merge), with the plain-merge boundary witnessed (a same-direction different-payload choice is a SAFE protocol that plain merge rejects). Honestly named projectable_wf (projection EXISTENCE, not safety); the general two_party → projectable_wf is not proved (it is false — two_party is strictly more permissive), so the n=2 collapse is witnessed by example. S3b done — static n-party configuration: the first n-party configuration form — role_assignment := list (role*party) + the In-based wf_assignment (every listed endpoint typed at its role's projection), with the binary Conf/wf_config recovered as the n=2 slice (conf_is_role_assignment2, reusing projected_config_wf) + converse embed, an n=3 non-Conf static witness over g_ring (wf_ra_ring), and honesty witnesses (duplicate-key tolerance → no functionality theorem; projectable_but_uncoverable → no general "projectable ⇒ coverable") — static only, wf_assignment = typed-at-projection NOT n-party safety, no operational n-party metatheory. S3c.0 done — full label-union merge: the Honda-Yoshida-Carbone umerge (keystone umerge_idem) added alongside the plain merge, unlocking different-label external (&) choices the plain merge rejects (witnessed umerge_widens_strictly); type-algebra only, and it does not unlock the different-payload g_excluded class (unions labels, not payloads). S3c.1 done — union-projection: a SEPARATE proj_u (plain proj with the uninvolved fold's merge replaced by umerge) added alongside proj (canonical proj/merge/projectable_wf byte-identical, NOT re-pointed), with the union projectability predicate projectable_u_wf, the keystone existence theorem projection_total_u (every role of a projectable_u_wf global type union-projects), and the one-directional monotonicity bridge projectable_wf_implies_u (every plain-projectable G is union-projectable, projections coinciding) riding on the keystone merge_forces_eq (plain merge is the identity-meet); non-vacuity g_union3 (uninvolved role sees &{3:end} vs &{4:end} — different labels) is genuinely in union-projectable minus plain-projectable; projection-EXISTENCE only (no n-party safety), the bridge is DOMAIN-INCLUSION (converse FALSE). S3c.2 done — n-ary located operational semantics: the first operational metatheory over an n-party config — a located reduction nstep (the located mirror of the fused binary cstep: one communication ra_set-updates exactly the two communicating roles) + ra_set + a global-type reduction gstep + closures nstar/gstar + the functional wf_assignment_f (wf_assignment_to_f keeps S3b green); the 3-party ring run 0→1→2→0 to all-QEnd is witnessed on both sides (ring_runs_to_end, g_ring_gsteps). Adequacy ONLY: the load-bearing nstep_breaks_wf_at_fixed_G proves nstep does not preserve wf_assignment_f at a fixed G (so n-party SR must be stated against a stepping G), no progress. S3c.3-msg done — head-coupled message subject reduction: the first EARNED n-party safety half — nstep_sr_msg_head proves the head communication carries wf from GMsg p q t G' to its continuation G' (3-way located role split; the SAME v:t the sender ships is what the receiver substitutes), coupled corollary nstep_gstep_sr_msg_head. The SAME ra_ring1 S3c.2 refuted at the fixed g_ring IS wf at the stepped g_ring (ra_ring1_wf_at_stepped_g, sealed by sr_earns_safety_across_step); the run-ahead fence is self-witnessed (runahead_breaks_head_coupling). Design-panel-validated + adversary-verified (sound-and-honest); HEAD message fragment, preservation only. Deferred: run-ahead/permutation SR (S3c.3-perm), select SR (S3c.3-choice), n-party progress (S3c.4 — research-hard, fence). A greenfield overtake — AffineScript@main (surveyed 2026-06-02) has no concurrency/session/π/multiparty metatheory in any form.
Echo in the type system (TEcho, MkEcho/Weaken, THEcho/THWeaken, EchoMode, EchoResidue)	locally-checked — Echo is a first-class type former in the formal kernel; EchoResidue backs the Rust Ty::Echo (5/5 unit tests are its laws)
Paper proofs (~6.3k lines)	proved-on-paper
Proof CI	present — proofs.yml machine-checks the Coq + Idris2 solo-cores (coqc + idris2 --build) on every PR touching proofs/verification/**, and asserts progress/preservation/affine_pres axiom-free

See proofs/AXIS-ARCHITECTURE.md for how the proof effort factors (resource / structure / modality / surface axes, and the resource↔echo non-identification invariant), and proofs/ALIGNMENT-PLAN.md for the phased roadmap toward AffineScript parity.

Echo type integration

my-lang integrates the echo-types Agda library — a formal account of loss that is not total erasure.

Echo<A => B>   // "a proof-relevant residue of a lossy collapse from A to B"

EchoMode { Linear, Affine } mirrors the EchoLinear.agda two-point poset linear ⊑ affine. A Linear echo may be weakened to Affine (one-way, no section). Domain and codomain are invariant under subtyping.

Claim boundary (retraction R-2026-05-18):

Echo is a loss-graded reindexing modality over a thin poset, not a graded comonad or free construction.

Full design rationale: docs/design/echo-types-integration.md.

Architectural authority

• ANCHOR.scope-arrest.* — the scope-arrest anchor enumerating what my-lang will and will not be.
• AUTHORITY_STACK.mustfile-nickel.scm — the cross-cutting authority stack.

Consult these before opening a feature request.

Status

• Licence: MPL-2.0
• Maturity: design-iteration / early alpha. Working Rust compiler core exists (137+ passing tests); surface syntax and semantics still settling.
• Proof phase: F1.4 done on the Coq track — QTT semiring + progress + preservation machine-checked (axiom-free, CI-guarded); Idris twin pending (Phase F5 parity). R2 done: the Coq solo core is now one functor SoloCoreF (M : SEMIRING) parametric over a resource-algebra interface — Include SoloCoreF Linear3 recovers the axiom-free result, and tropical/affine instances fall out (R4 done: SoloCoreF Tropical is verified axiom-free at an infinite min-plus carrier). R3 done: affine_pres is now a distinct theorem — affine budget-preservation over ule (pointwise qle), not an alias of preservation — with the functor parameter widened to ORDERED_SEMIRING. R5 done (F1.4 tail): the declarative static context-splitting judgement is proved equivalent to an executable one-pass usage-walk checker check — check_correct : has_type G D t a ↔ check G t = Some (a, D) is axiom-free Qed., the spec for the Rust dialects/solo checker; it inherits to the infinite tropical carrier for free and overtakes AffineScript (which leaves this equivalence as prose "future work"). M1.0/M1.1/M1.1b done (2026-06-14): the visual me surface now elaborates into the solo core (elab, a core-landing analogue of the paper translate) with a machine-checked, axiom-free Visual-Soundness theorem (elab_data_check) for the no-linear-use data fragment — and M1.1b a me typing judgement (me_wt/me_wt_sound) making the linear-use constructs (token-consume, MeLet, pair-split, the faithful MeIf → Case) universal over the whole me_tm (incl. MeSeq) — M1 complete. For that fragment it is the first mechanised surface→core elaboration correctness in either sibling, as surveyed against AS@main 2026-06-02 (axis-4 SURFACE rung M1). S1 + S2 done (2026-06-14): the structure climb (axis-2) is mechanised in the standalone Coq development SessionPi.v — a synchronous binary session-typed π-calculus core (session types + computed duality, polarised endpoints, a linear channel-typing judgement, small-step reduction) with subject reduction (sr_comm, config_subject_reduction), session fidelity (session_fidelity) and progress / deadlock-freedom (config_progress) for the binary fragment (S1.0–S1.2), and the duet-by-projection layer (S2.0/S2.1) — multiparty-shaped global types, the three-case projection, projection_duality, and corollaries that transport the whole S1 guarantee across projection so a projected choreography is deadlock-free by construction — all axiom-free and CI-guarded. S1.3 done (2026-06-14): n-ary labelled choice (S1.3a, the three fused theorems extended), structural congruence preserves typing (S1.3c, wt_congr), and the equi-recursive μ type-layer (S1.3b-core: unfold_mu/dual_unfold/guarded). S2.2 done (2026-06-14): global-type labelled choice (GBra) + equi-recursive (GMu/GVar) projection — projection is now partial (option sty) with a plain merge (keystone merge_idem) for uninvolved roles and projection_duality reproved in option-map form over choice + μ; fenced as plain (not union) merge, unpruned μ, no global-level metatheory. S3a done (2026-06-14): the first n≥3 theorem — projection_total (every role of a projectable_wf global type projects), breaking the "no theorem quantifies over a genuine n-party system" fence. S3b done (2026-06-14): the first n-party configuration form — role_assignment + the In-based wf_assignment, the binary Conf recovered as the n=2 slice (conf_is_role_assignment2, reusing projected_config_wf), an n=3 non-Conf witness over g_ring, and honesty witnesses (duplicate keys; projectable-but-uncoverable); static only — wf_assignment = typed-at-projection NOT n-party safety. S3c.0 done (2026-06-14): the full label-union merge umerge (keystone umerge_idem) added alongside the plain merge — type-algebra only, unlocks different-label & choices (not the different-payload class). S3c.1 done (2026-06-14): a SEPARATE union-projection proj_u (the only token changed from proj is merge→umerge in the uninvolved fold) + projectable_u_wf + the keystone existence theorem projection_total_u + the one-directional monotonicity bridge projectable_wf_implies_u (on the keystone merge_forces_eq: plain merge is the identity-meet); canonical proj byte-identical, projection-EXISTENCE only, non-vacuity g_union3 genuinely in union-projectable minus plain-projectable. S3c.2 done (2026-06-14): the first operational metatheory over an n-party config — a located reduction nstep (located mirror of the fused cstep) + ra_set + a global gstep + nstar/gstar + the functional wf_assignment_f (wf_assignment_to_f keeps S3b green); the 3-party ring run witnessed both sides (ring_runs_to_end, g_ring_gsteps); adequacy ONLY — nstep_breaks_wf_at_fixed_G proves no fixed-G subject reduction. S3c.3-msg done (2026-06-14): the first EARNED n-party safety half — nstep_sr_msg_head (head-coupled message subject reduction, 3-way located role split), coupled corollary nstep_gstep_sr_msg_head, the earned-safety headline sr_earns_safety_across_step (the same ra_ring1 S3c.2 refuted at the fixed g is wf at the stepped g), and the self-witnessed run-ahead fence runahead_breaks_head_coupling; adversary-verified sound-and-honest. Remaining: μ typing/SR up-to-unfolding (S1.3b-meta, deferred), select SR (S3c.3-choice), run-ahead SR (S3c.3-perm), n-party progress (S3c.4). A greenfield overtake — AS has no concurrency/session/π/multiparty metatheory in any form (surveyed AS@main 2026-06-02).
• Governance: CI green on all shipped checks; proof CI live (proofs.yml machine-checks the solo-cores).

Contributing

See CONTRIBUTING.adoc. GPG-signed commits required. Language policy, package management, and security requirements are enforced by the estate governance workflow (hyperpolymath/standards). New contributors should read EXPLAINME.adoc first.

Companion repositories

Repository	Relationship
hyperpolymath/standards	Estate-wide standards and governance
hyperpolymath/affinescript	Sibling language; target parity state defined in proofs/ALIGNMENT-PLAN.md
hyperpolymath/echo-types	Upstream Agda echo-types library integrated into the type checker
hyperpolymath/EchoTypes.jl	Julia companion; planned differential oracle for echo type testing
hyperpolymath/typed-wasm	Shared typed-wasm compilation backend