Doxa
previewA dependently typed proof checker
A proof checker for the Calculus of Inductive Constructions, with an ML-family surface syntax. You write data types, functions, and proofs; Doxa checks that the proofs actually establish the theorems you state. Rumil parses the source into a surface tree; the elaborator, type checker, and normalizer are Doxa's own. It compiles to WebAssembly and runs entirely in the browser, with no server, in about 76KB. Preview: the kernel is complete and the standard library type-checks end to end, but the language is still settling and has not had a tagged release.
Examples
A data type, a function, and a proof that addition has a right identity
Data types declare their constructors. Type parameters go in square brackets at the declaration; constructors infer them at use. (Edit any example; it re-checks as you type.)
Functions use `fun`. Explicit parameters take round brackets; implicit ones, that the checker solves for, take curly brackets.
Equality is the prelude type `Eq`. A reflexive proof is `refl`, checking by computation.
When a proof does not hold, the checker says so, and points at the term that does not fit. Try fixing it.