What is Cella?
Cella is a programming language for formal verification and proof. Its core is cubical type theory (CCHM); the same syntax also has quantities (QTT), modalities (MTT), definitional proof irrelevance (SProp) and user-declared rewrite rules, and a definition’s mode decides which of these it may use (see Type theories). Cella is a proof assistant, and it also writes and runs ordinary programs.
What it gives you
Section titled “What it gives you”- A verdict for every check: Accept, Reject or Unknown, each saying what it rests on (see Verdicts).
- Proofs with tactics (
rfl,intro,induction,simp,ring,omega,linarith,decide, …) andcalc. The arithmetic tactics find a certificate in Rust and check it by computation in Cella; the solver finds, it does not judge. - Programs with
IO, strings and arbitrary-precisionNat, on three backends: WasmGC (the default), a bytecode VM and a normalization-by-evaluation interpreter. Type checking and running are two projections of the same semantics. - Holes: a program with
?namein it is Unknown, and Cella lists each hole’s type and context, and what fits it.
Programming languages as Cella programs
Section titled “Programming languages as Cella programs”The semantics of C11, C++17, Arduino and ESP32 boards, and Python are written in Cella as deep embeddings. A program is a syntax tree; its type checker reports errors at the offending node, and its small-step semantics runs it. The verdict says whether it ran to the end, broke a rule of the standard (and which clause), or depends on a choice the standard leaves to the implementation. See Packages.
Where it is used
Section titled “Where it is used”Cella’s first application is semorphe, an editor that teaches programming with blocks and code; lessons on Cella itself will move there. The second is an operating system for WebAssembly, for which Cella is the toolchain and the verifier.