Project Status

Project Status

Measured 2026-08-07 against commit e68bb3d.

Authoritative sources, in precedence order:

1. proofs/STATUS.md — for proofs
2. .machine_readable/6a2/STATE.a2ml — for everything else
3. DEBT.md — for what is known-broken

Measured

Version	0.2.0 — early alpha, experimental. No tagged release.
Tests	221 pass, 0 failures (cargo test --workspace --exclude my-llvm)
Coverage	~46.7% baseline; CI floor set at 40%
Workspace	15 crates
Proofs	Coq ~8.7 kLOC + Idris2 ~2.5 kLOC; zero Admitted/holes
Live dialect	Solo only
Licence	MPL-2.0 (code), CC-BY-SA-4.0 (docs)

What works

• parse → HIR → MIR → LLVM → native on x86_64 and aarch64
• Solo dialect end-to-end via the interpreter and the native pipeline
• Both proof tracks build; the Coq track is axiom-free gated per rung in CI

What doesn't

• #typeck (high) — the Rust checker is tested against, not proved equal to, the verified check. The headline correctness goal.
• No async/await, channels, or concurrency runtime in the surface language
• AI surface performs mock operations
• my-pkg cannot resolve or install; my-lsp has six unimplemented handlers
• Duet and Ensemble are proofs plus scaffolding, not usable compilers

Debt at a glance

DEBT.md catalogues 34 items across seven domains — 8 high, 21 medium, 5 low.

Domain	Highlights
Licence	An undefined SPDX identifier (Palimpsest-0.8); MIT declared with no MIT text; two LICENSE files whose SPDX tag contradicts their body
Documentation	Wiki pages documenting an installer, a std:: tree, and async that do not exist — now carrying warning banners
Code	~7,300 LOC of orphaned duplicate source in root src/ and lib/; a stub my-parser crate that always succeeds
Proof	The proof workflow doesn't re-run when the implementation changes; the Idris job has no hole assertion
Test	34 property tests that are never compiled; coverage floor below the current baseline
CI/CD	Actions-lockfile regeneration is a recurring manual step after every dependabot bump
Metadata	ECOSYSTEM.a2ml staleness; a K9 self-validation file whose own rules the tree violates

Roadmap

Next rungs, per STATE.a2ml:

1. S3c completion — select/branch SR, permutation SR, then n-party progress (research-hard, explicitly fenced)
2. S1.3b-meta — μ typing / SR up-to-unfolding
3. F1.2 — four-point affine semiring (0 ⊏ ? ⊏ 1 ⊏ ω)
4. Echo stage 2 — Echo<A => B> surface syntax

Full detail, including an explicit Not planned section, in ROADMAP.adoc.