Why Li is mathematically provable¶
“Mathematically provable” means: the important properties of your program are theorems checked by a small, trusted proof engine — not hopes backed by testing alone.
The proof gate¶
Today: lic build runs parse, policy, typecheck, borrow, and codegen — without Lean yet. See Provability gaps.
When Phase 2f lands: if Lean still has open goals, no executable ships.
What is being proved?¶
| Claim | Mechanism |
|---|---|
| Types line up | Typechecker |
| Indices in range | Refinements + VCs |
| Memory safe | Borrow checker |
| Preconditions hold | requires / ensures |
| Loops terminate | decreases |
| Parallel loops race-free | Disjointness + Sync laws |
| No escape hatches | Reject Any, sorry, bare cast |
Together, these are stronger than “we fuzzed it.”
Why Lean 4?¶
Lean’s kernel checks proof terms. If the kernel accepts a proof, the logical chain is valid relative to the axioms you started from.
Li is not “SMT said maybe” or “tests passed” — it is proof objects checked by the kernel.
This is the same assurance culture as Coq-style verification, using Lean 4 as the engine.
What you write vs what Lean sees¶
You write Nim-like code with contracts. The compiler:
- Typechecks and borrows.
- Generates verification conditions (VCs).
- Sends obligations to Lean.
- Only then emits LLVM.
So the binary is a compiled proof artifact, not a separate “verified mode.”
Trusted axioms (minimal)¶
Real programs need a little I/O. Li keeps a small trusted file:
docs/semantics/trusted.lean
Only this file may contain unproved axioms (bounded, reviewed). Application logic stays in user code with full contracts.
Honest limits¶
| Limit | Explanation |
|---|---|
| Implementation gaps | Features listed in the spec but not fully proved yet — gap register |
| Wrong spec | You can prove the wrong theorem perfectly |
| Trusted base growth | Must stay tiny and audited |
| Compiler correctness | Proving the C++ compiler matches Lean is future meta-work |
| CPU behavior | Proofs are about the Li model, not flaky hardware |
Parallelism and proof¶
Shared-memory parallelism is the hardest part of HPC correctness. Li’s answer: reject parallel for unless disjointness is stated and checked. See li-tests/race_shared_memory/.