Lean
Blog
Programming Language and Theorem Prover