Does anyone know the origin of the quote,

Informal proofs are algorithms; formal proofs are code.

Its made in Benjamin C. Pierce et al.'s Software Foundations.


1 Answer 1


He doesn't cite any references for it and Google doesn't return any results so I don't think he is really quoting from anywhere.

The idea that a proof is a "construction" (a term in intuitionistic/constructive mathematics with a very close meaning to what we call algorithm nowadays) goes back to at least Luitzen Egbertus Jan Brouwer. Note that Brouwer was talking about informal proofs as typically stated by mathematicians, not formalized proofs which are a very recent phenomenon.

The idea that a formal proof is a like a program in a programming language can be traced back to at least to the BHK interpretation of intuitionistic logic by Arend Heyting. The formal correspondence is Curry-Howard isomorphism.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.