A theorem prover that is also an ergonomically sensible programming language.