Programming Proofs and Proving Programs

Speaker  Nick Benton

Affiliation  MSRC

Host  Scarlet Schwiderski-Grosche

Duration  00:55:47

Date recorded  2 July 2013

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.

©2013 Microsoft Corporation. All rights reserved.
> Programming Proofs and Proving Programs