# 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.