Vow

Vow is an experimental programming language designed for a machine author. Its guiding rule is that every function should be checkable from its signature alone. Effects are declared in the signature, contracts are proved by the Z3 SMT solver every time you compile, and nothing depends on operator precedence or on context far away.

Refinement types, preconditions and postconditions, loop invariants, termination measures, index bounds and division by zero are all proof obligations, and a failed proof comes with a counterexample. Typed holes report the expected type and every fact the compiler knows at that point. The idea is that when a coding agent writes the code, people can review its contracts instead of its bodies.

The compiler is written in Vow, about 6,000 lines, and verifies itself: every index and refinement in it is proved, and compiling it with itself gives byte-identical C. It went from spec to self-hosting in a day, bootstrapped by a Rust compiler, and has since gained modules, packages and refined generics, along with independent soundness reviews and fuzzing. It’s one of my Lean Machine experiments, released under the Unlicense and installable with Homebrew.