Cure v0.35.0 :: Mechanised Soundness, Tree-Sitter & Kernel Hardening

Cure v0.35.0 marks a profound moment of mathematical rigor and developer experience for the language.

In v0.34.0, Cure unified its compiler into a single dependent pipeline: every .cure program elaborates into a small, kernel-checked Core calculus before quantitative erasure and BEAM emission. But building a dependent type theory on the BEAM raises an inescapable question: how do we know the trusted kernel is actually sound?

Following an intensive, independent technical audit (AUDIT-20261009.md), v0.35.0 delivers what very few languages running on production virtual machines can claim: an exhaustive written soundness argument (docs/SOUNDNESS.md) and an essentially complete machine-checked formalisation in Agda (proof/).

Alongside this metatheoretic milestone, v0.35.0 brings first-class editor integration with a brand new lexical Tree-Sitter grammar (tree-sitter-cure/) and an upgraded Zed editor extension (zed-cure/), alongside critical audit-driven kernel hardening—including a strict code-generation firewall for typed holes and enforced compile-time @total true certification.

Author Credits

This release reflects key contributions across metatheory and developer tooling:

• Aleksei Matiushkin (@alekseylm): Designed and authored the formal soundness specification in docs/SOUNDNESS.md, implemented the ~6,000-line machine-checked Agda proof in proof/, and resolved the core compiler audit obligations.
• Pedro Fonseca (@pedrohfonseca81): Designed and authored tree-sitter-cure, providing a robust lexical grammar mirroring Cure's lexer, and rebuilt the zed-cure extension for Zed.

The Agda Soundness Proof (proof/)

The core thesis of Cure is that industrial OTP concurrency can live harmoniously with proof-assistant-grade type theory. In v0.35.0, that type theory graduates from "tested by property fuzzers" to mechanically verified.

The formalisation in proof/ models the Core calculus of Cure.Core.Term:

• A three-level universe hierarchy (Type 0 : Type 1 : Type 2).
• Graded dependent functions ($\Pi$) with Quantitative Type Theory (QTT) usage grades ${0, 1, \le 1, \omega}$.
• Graded $\zeta$-transparent let bindings.
• Indexed inductive families (GADTs) with dependent eliminators (case).
• Totality-gated $\delta$-unfolding for global references.
• Inert effect formers (Effect, pure, bind) with zero reduction rules.

The Soundness Theorem

Theorem (Soundness). Let $e$ be a closed, hole-free, final-Core term with $\cdot \vdash e : T$ for a closed type $T$. Then evaluation of $e$ either:

1. Reaches a value $v$ with $\cdot \vdash v : T$; or
2. Raises an exception (coverage or partial-op guard); or
3. Diverges.

In particular, evaluation never reaches a stuck state: a well-typed closed term is never a neutral eliminator whose scrutinee is a value.

-- The bounded outcome by induction on fuel:
soundness-fuel : ∀ (n : ℕ) {t T} → ⟨⟩ ⊢ t ⇐ T → Final t → FuelResult t T

-- The coinductive completion by guarded corecursion:
soundness-tree : ∀ {t T} → ⟨⟩ ⊢ t ⇐ T → Final t → EvalTree t T

-- The classical three-way theorem:
soundness : ∀ {t T} → ⟨⟩ ⊢ t ⇐ T → Final t → EvalResult t T

Proved Lemmas & Key Findings

1. Progress (Proof.Progress): Proved by mutual induction on typing derivations. A well-typed closed term is either a canonical value, a neutral term, or can step.
2. Preservation (Proof.Preservation): Fully proved with zero postulates across every single reduction rule:
   • $\beta$ and $\zeta$ cases: The inference-preservation gap was cleanly dissolved by proving check-infer (every hole-free term that checks against a type also infers it).
   • $\iota$ (case elimination): Branch substitution is proved by typing branch field binders with the constructor's actual argument telescope (extendTele), with compact literal peeling for Nat and Bounded.
   • $\delta$ (unfolding): Proved via CertifiedTyped and weaken-closed, guaranteeing certified functions remain type-safe upon expansion.
   • $\xi$-congruence: Context conversion and motive conversion (branches-conv) preserve typing across evaluation contexts.
3. Canonical Forms & Head Inversion (Proof.CanonicalForms, Proof.Inversion): Proved that terms checking as function or data types evaluate strictly to canonical introductions.
4. Simultaneous Substitution (Proof.Substitution, Proof.Context): Rebuilt on length-indexed contexts (Ctx n) with Fin index lookups, establishing the complete algebra of weakening and substitution interactions.

The development compiles cleanly under Agda and can be verified via ./proof/check.sh.

Written Soundness Specification (docs/SOUNDNESS.md)

Complementing the Agda formalisation, docs/SOUNDNESS.md provides an exhaustive, readable specification of the trusted computing base (TCB, ~9,200 LOC in lib/cure/core/).

The document catalogs the three load-bearing side conditions that protect the kernel from inconsistency:

1. Strict Positivity: Enforced by Inductive.positive?/2 via nested, cycle-guarded traversal, barring negative recursive occurrences like MkBad : (Bad -> Nat) -> Bad that would allow non-terminating loops without recursion.
2. Totality-Gated $\delta$-Reduction: Unfolding during definitional equality conversion (Cure.Core.Conv) is permitted only for definitions accompanied by a valid Lee–Jones–Ben-Amram size-change totality certificate, preventing the type checker itself from looping.
3. Coverage & Branch Unification: Dependent case elimination requires exhaustive branch coverage validated through structural first-order index unification.

Tree-Sitter Grammar & Zed Editor Support

Thanks to Pedro Fonseca, Cure now features a full, standalone Tree-Sitter grammar and an upgraded Zed editor integration:

tree-sitter-cure/

• Designed to mirror Cure.Compiler.Lexer with zero external runtime dependencies.
• Handles Cure's lexical structure, operators, sigils, and line-boundary semantics.
• Treats line boundaries as tokens so highlight queries recognize macro vocabulary (syntax family, accepts, expands with, family fields) at line starts.
• Verified against every .cure file in the entire repository with zero parse errors.

zed-cure/

• The extension now bundles and builds directly from the in-tree tree-sitter-cure/ grammar.
• Complete tree-sitter queries for syntax highlighting (highlights.scm), symbol outlines (outline.scm), bracket matching (brackets.scm), and indentation rules (config.toml).
• Provides seamless, lightning-fast editing in Zed.

Compiler Hardening & Audit Resolutions

The technical audit in AUDIT-20261009.md identified several practical friction points and safety oversights. Release v0.35.0 resolves each one directly:

1. The Hole Firewall (Audit §4.2)

While typed holes (?goal) are invaluable during interactive development, they must never escape into production binaries. Previously, unfilled holes could bypass codegen checks under certain compilation paths.

• Enforcement: Emit.reject_holes/2 now guards every code-generation entry point. Any attempt to compile an artifact containing an unfilled hole immediately halts emission with diagnostic E014 ({:codegen_error, {:unfilled_hole, details}}).
• Pinned with regression suites in test/cure/elab/hole_firewall_test.exs.

2. Enforced @total true Decorator (Audit §4.3)

The @total true annotation previously served as an unenforced decorator on non-type-level functions.

• Enforcement: Cure.Elab.Declarations now records explicit totality obligations on the environment. The compiler rejects any function decorated with @total true with diagnostic E013 unless the size-change termination checker certifies structural descent.
• @total false provides an explicit opt-out.

3. Dedicated E123 Diagnostic for Missing Module Identity

When compiling multi-file projects, macro containers missing an explicit module declaration previously crashed with an uninformative POSIX error: module_identity_missing. This is now intercepted cleanly and surfaced as a standard compiler diagnostic:

-- MODULE IDENTITY MISSING [E123] ----------------------------------------------

4. Standard Library Consistency (Audit §4.6)

• Normalized unwrapping functions across Std.Option and Std.Result. Both modules now provide consistent unwrap and unwrap_or signatures with matching semantics.
• Verified with comprehensive consistency assertions in test/cure/stdlib/consistency_test.exs.

5. Cross-Platform CI

• Added dedicated macOS build automation to GitHub Actions (.github/workflows/ci.yml), resolving architecture-specific build failures and ensuring multi-platform parity.

Summary of Changes

Looking Ahead

Cure v0.35.0 bridges the gap between ambitious language design and foundational mathematical proof. By proving type preservation and progress in Agda while simultaneously expanding editor support and tightening compiler invariants, Cure proves that a dependently-typed systems language on the BEAM is not just viable, but rigorously sound.

To test your code with the updated compiler, install Cure v0.35.0, run cure check, and explore the formal proof in proof/README.md.