Soundness Claims

Status: stub

Full soundness documentation is planned for Phase 2. This stub covers the evidence grading system used in the spec.

Spec source: THEOREMS.csl

Evidence grading

The compiler spec (THEOREMS.csl) grades each soundness claim with one of four evidence levels. These are published honestly — overclaiming soundness that doesn’t exist is worse than publishing an honest partial result.

Symbol	Grade	Meaning
✓	Proven	Formal proof exists and has been checked
◐	Partial	Proof holds under stated restrictions; full generality not yet proven
○	Informal	Argument exists but no formal proof; believed sound
✗	Unproven	Claim is conjectured; no proof attempted yet

The KB will display these symbols next to theorem statements when the full soundness page is written. Theorems with ○ or ✗ status are labeled as such — they are not presented as proven.

Key soundness goals

• Effect soundness: a program typed as !pure performs no observable side effects at runtime
• GPU/CPU separation: no !gpu function is reachable from CPU execution without passing through a pipeline boundary
• Autodiff correctness: the derivative computed by ∂f is mathematically correct for all Differentiable inputs
• Capability unforgability: capabilities cannot be constructed by user code; they can only be obtained from the runtime

Status of formal proofs for each: coming in Phase 2.