Programming Proofs and Proving Programs

Developers turn coffee into programs, whilst mathematicians turn it into proofs. Amazingly, proofs and programs are not just made from the same stuff, but there’s a strong sense in which they actually *are* the same stuff. The modern understanding of proofs, programs, and the correspondence between them, is one of the most significant intellectual developments of the 20th century. That understanding is now embodied in a radically new kind of language and software tool that could revolutionize both mathematics and software development in the 21st century.