Where is the quote "Informal proofs are algorithms, formal proofs are code" from? 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.
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.