<p>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.</p>

<p>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 <a href="https://en.wikipedia.org/wiki/L._E._J._Brouwer" rel="noreferrer">Luitzen Egbertus Jan Brouwer</a>.
Note that Brouwer was talking about informal proofs 
as typically stated by mathematicians, 
not formalized proofs which are a very recent phenomenon.</p>

<p>The idea that a formal proof is a like a program in a programming language
can be traced back to at least to 
the <a href="https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation" rel="noreferrer">BHK interpretation</a> of intuitionistic logic by <a href="https://en.wikipedia.org/wiki/Arend_Heyting" rel="noreferrer">Arend Heyting</a>.
The formal correspondence is <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="noreferrer">Curry-Howard isomorphism</a>.</p>

CC BY-SA 3.0
2016-05-19T22:08:47.573Z
2016-05-19T22:08:47.573Z
Kaveh
<p>Does anyone know the origin of the quote,</p>

<blockquote>
  <p>Informal proofs are algorithms; formal proofs are code.</p>
</blockquote>

<p>Its made <a href="https://web.archive.org/web/20170512232112/https://www.cis.upenn.edu/~bcpierce/sf/current/Induction.html#lab48" rel="nofollow noreferrer">in Benjamin C. Pierce et al.'s Software Foundations</a>.</p>

<reference-request><proofs><proof-assistants>
Where is the quote "Informal proofs are algorithms, formal proofs are code" from?
Steven Shaw
# Where is the quote "Informal proofs are algorithms, formal proofs are code" from?

(Asked by: username_0 on 2016-05-18)

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](https://web.archive.org/web/20170512232112/https://www.cis.upenn.edu/~bcpierce/sf/current/Induction.html#lab48).

**Tags:** reference-request, proofs, proof-assistants


---

## 1 answers

### Answer by username_1 on 2016-05-19. Score: 5

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](https://en.wikipedia.org/wiki/L._E._J._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](https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation) of intuitionistic logic by [Arend Heyting](https://en.wikipedia.org/wiki/Arend_Heyting).
The formal correspondence is [Curry-Howard isomorphism](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence).


---

