<p>The programming languages people use day to day don't fit so well into the Curry-Howard correspondence, because their type systems are too weak. To say something interesting using Curry-Howard for imperative programs, one needs to have a more sophisticated type system. The book <a href="http://rads.stackoverflow.com/amzn/click/0387237593">Adapting Proofs-as-programs</a> pushes this angle with the aim of synthesising imperative programs. With dependent types becoming more and more popular, certainly in research functional languages (<a href="http://wiki.portal.chalmers.se/agda/pmwiki.php">Agda</a>, <a href="http://www.e-pig.org/darcs/Pig09/web/">Epigram</a>), the distinction is becoming blurrier. Of course you can do program synthesis/extraction within the <a href="http://coq.inria.fr/">Coq</a> theorem prover (and presumably others), which is of course based on Curry-Howard.</p>

<p>The Curry-Howard correspondence can also be used in situations where the proofs do not so clearly correspond to programs (or they are not programs anyone will ever run). One example of this is in <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.129.1811&amp;rep=rep1&amp;type=pdf">Proof-carrying authorization</a>. The propositions correspond to statements about who is authorized to do what. Proofs provide the required evidence that a proposition holds, thus an authorization request is permitted. In order to encode the proofs, proof terms are introduced (via Curry-Howard). Proof terms are sent between parties as representations of proofs of the validity of authorization requests, but they are not considered programs.</p>

CC BY-SA 2.5
2011-03-01T20:22:02.080Z
You should mention dependently typed languages, as in them the line between proofs and propositions gets  blurred.
Ohad Kammar
CC BY-SA 2.5
2011-03-01T20:25:43.217Z
Indeed. Let's not forget Coq's program synthesis/extraction.
Dave Clarke
CC BY-SA 2.5
2011-03-02T07:40:07.087Z
what program would correspond to a non-constructive (classical) proof of the form $\forall k \ T(e,k) \lor \lnot \forall k \ T(e,k)$? (Assume that $T$ is some interesting decidable relation e.g. $e$-th TM halts in $k$ steps.) (I can ask it as a new question if the answer is not very short.)
Kaveh
CC BY-SA 2.5
2011-03-02T08:27:55.457Z
@Kaveh: do ask this as a separate question. In a comment you can say "the Godel-Gentzen translation is a continuation-passing transformation" but anything less cryptic won't fit. :)
Neel Krishnaswami
CC BY-SA 2.5
2011-03-02T10:48:36.083Z
@Neel, done: http://cstheory.stackexchange.com/q/5245/186
Kaveh
CC BY-SA 2.5
2011-03-01T19:28:15.623Z
2011-03-01T20:32:38.610Z
2011-03-01T20:32:38.610Z
Dave Clarke
<p>In Coq, there are 2 types (Prop and Set), they are used by the programmer to separate what are proofs that won't produce actual code and the part of the proof that will be used to extract running code (your program).</p>

<p>That is a nice solution for the problem you ask about, how to identify what is meant to generate machine code (program) and what is present to complete the proof of the proposition (or type). </p>

<p>AFAIK there is no automatic way to distinguish both. This might be something interesting for research? Or maybe someone is able to point out it's clearly impossible?</p>

<p>With dependent types not only there isn't a clear distinction between proofs and programs but also there isn't a distinction between programs and types!
The only distinction will be where the type(or program) appear, making it part of the "program" place or of the "type" place of a given term.</p>

<p>An example will make it clearer i hope:</p>

<p>When you use the identity function with dependent types you need to pass the type your are going to use the function with! The type is being used as a value in your "program"!</p>

<p>Untyped Lambda Calculus:</p>

<p>id = $\lambda{x}.x$</p>

<p>With Dependent Types:</p>

<p>id : (A : Set) -> A -> A</p>

<p>id = $(\lambda{A}.(\lambda{x}.x))$</p>

<p>If you are using this function, then you would do it like this example:</p>

<p>id Naturals 1</p>

<p>Notice that the "type" (in this case the Set of Naturals) being passed as a value is thrown away so it will never be computed, but still it's in the "program" part of the term. That's what also will happen with the "proof" parts, they need to be there for the term to type-check but during computation they will be thrown away.</p>

CC BY-SA 2.5
2011-03-02T01:56:41.000Z
2011-03-02T02:14:38.323Z
2011-03-02T02:14:38.323Z
Flávio Botelho
<p>I will go out on a limb here and say that, if you are willing to squint a bit, proofs and <strong>terminating</strong> programs can be identified.</p>

<p>Any terminating program is a proof that you can take its input and produce its output.  This is a very basic kind of proof of implication.  </p>

<p>Of course, to make this implication carry information more meaningful than stating the obvious, you need to be able to show that the program works for any and all instances of input drawn form some class with logical meaning. (And so too for the output.)</p>

<p>From the other direction, any proof with finite inference steps is a symbolic program manipulating objects in some logical system. (If we don't worry too much about what the logical symbols and rules mean computationally.)</p>

<p>Types and propositions can be made to work similarly.  Any type T can be assigned the proposition $\exists x : x \vdash T$ with obvious truth conditions.  Any proposition can be turned into the type of it's proofs.</p>

<p>This is pretty simplistic, but I think it does suggest the robustness of the idea.  (Even if some people are bound not to like it. ;-) )</p>

CC BY-SA 2.5
2011-03-05T15:36:48.283Z
I think this is a bit tricky, depending on how you are defining finite and infinite with respect to proofs.  In general, all proofs that we accept are finite, because they have to convince a human in a small finite amount of time.  A proof that relies on an induction scheme (i.e. most "infinite" proofs) are by this measure still finite, they just have symbolic steps that represent an infinite but regular computation.  A truly infinite proof, that I think most of us would reject as a valid proof, would be one where you literally had to consider an infinite number of distinct facts to validate.
Marc Hamann
CC BY-SA 2.5
2011-03-03T22:15:17.467Z
very good answer.
toto
CC BY-SA 2.5
2011-03-05T02:32:39.867Z
One should assume, of course, that you mean **finite** proofs and terminating programs. Some classes of non-terminating programs work just fine as infinite proofs. It's the non-productive non-terminating programs you need to watch out for.
wren romano
CC BY-SA 2.5
2011-03-02T00:02:26.267Z
2011-03-02T00:02:26.267Z
Marc Hamann
<p>Proof irrelevance?</p>

<p>When you write some program, you are interested in its performance, memory consumption etc.<br>
E.g it's better to use some clever sorting algorithm instead of bubble sort, even if their implementations have same types (even in dependent type setting).</p>

<p>But when you prove some theorem it is only existence of a proof you are interested in.</p>

<p>Of course, from aesthetic point of view, some proofs are more simple/beautiful/inspiring/etc (e.g. proofs from The Book).</p>

CC BY-SA 2.5
2011-02-28T13:27:29.003Z
2011-02-28T13:27:29.003Z
max taldykin
<p>If you accept the Curry–Howard correspondence then the question is mainly a philosophical one. "Are proofs and programs different? Of course. How? Well, we call proofs 'proofs' and we call programs 'programs'."</p>

<p>Or to put it less flippantly, if there's an isomorphism between proofs and programs —which it seems clearly there is— then your question is asking whether there is any oracle capable of distinguishing the two. Humans categorize them as being different (for the most part), so it's certainly arguable that such an oracle exists. The important question then becomes whether there is any <em>meaningful</em> difference between them, which is up for philosophical debate. What is a "proof"? There is no formal definition of what constitutes a proof; it's a term of art, much like the notion of "effectively calculable" in the Church–Turing thesis. For that matter, "program" has no formal definition either.</p>

<p>These are words of natural language used to categorize different fields of mathematical enquiry. What Curry and Howard observed is that these two different fields where in fact studying the same thing. Noticing this connection is important because it says that these different researchers should be talking to one another. But on another level, to notice the connection is to belie the difference between them. When tackling a problem, sometimes it is more beneficial to think of it as a programming problem, whereas other times it is more beneficial to think of it as a logical problem. This difference in perspective is, I think, the important difference between them. But whether a difference of perspective constitutes a difference of identity is a deep philosophical question which has been explored at least as far back as Frege's <em>Ueber Sinn und Bedeutung</em>.</p>

CC BY-SA 2.5
2011-03-05T02:54:43.413Z
2011-03-05T02:54:43.413Z
wren romano
<p>Given that the <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">Curry-Howard Correspondence</a> is so widely spread/extended, is there any difference between proofs and programs (or between propositions and types)? Can we really identify them?</p>

CC BY-SA 2.5
2011-02-28T15:05:42.973Z
John Crossley wrote a paper on this that I happened to see posted somewhere recently: [What is the difference between proofs and programs?][http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.59.4712&rep=rep1&type=pdf] -- I haven't read it yet, but it came recommended...
Tara
CC BY-SA 2.5
2011-02-28T16:30:09.540Z
@TJ Ellis, thanks for the link, but after a brief skim, it seems that the paper doesn't answer the question posed in it's title (or the answer is "they are the same").
max taldykin
CC BY-SA 2.5
2011-03-08T16:28:31.410Z
@max @plmday heh, look at that... yeah, I did see it on r/compsci; I thought it was remarkable that such an appropriate question came up right after I had seen that... and no, I never did read it; it ended up languishing behind work windows and eventually was closed...
Tara
<lo.logic><pl.programming-languages>
What is the difference between proofs and programs (or between propositions and types)?
day
# What is the difference between proofs and programs (or between propositions and types)?

(Asked by: username_0 on 2011-02-28)

Given that the [Curry-Howard Correspondence](http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) is so widely spread/extended, is there any difference between proofs and programs (or between propositions and types)? Can we really identify them?

**Tags:** lo.logic, pl.programming-languages

> **Comments:**
> **username_1**: John Crossley wrote a paper on this that I happened to see posted somewhere recently: [What is the difference between proofs and programs?][http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.59.4712&rep=rep1&type=pdf] -- I haven't read it yet, but it came recommended...  
> **username_2**: @TJ Ellis, thanks for the link, but after a brief skim, it seems that the paper doesn't answer the question posed in it's title (or the answer is "they are the same").  
> **username_1**: @max @plmusername_0 heh, look at that... yeah, I did see it on r/compsci; I thought it was remarkable that such an appropriate question came up right after I had seen that... and no, I never did read it; it ended up languishing behind work windows and eventually was closed...  

---

## 5 answers

### Answer by username_3 on 2011-03-01. Score: 20

The programming languages people use username_0 to username_0 don't fit so well into the Curry-Howard correspondence, because their type systems are too weak. To say something interesting using Curry-Howard for imperative programs, one needs to have a more sophisticated type system. The book [Adapting Proofs-as-programs](http://rads.stackoverflow.com/amzn/click/0387237593) pushes this angle with the aim of synthesising imperative programs. With dependent types becoming more and more popular, certainly in research functional languages ([Agda](http://wiki.portal.chalmers.se/agda/pmwiki.php), [Epigram](http://www.e-pig.org/darcs/Pig09/web/)), the distinction is becoming blurrier. Of course you can do program synthesis/extraction within the [Coq](http://coq.inria.fr/) theorem prover (and presumably others), which is of course based on Curry-Howard.

The Curry-Howard correspondence can also be used in situations where the proofs do not so clearly correspond to programs (or they are not programs anyone will ever run). One example of this is in [Proof-carrying authorization](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.129.1811&rep=rep1&type=pdf). The propositions correspond to statements about who is authorized to do what. Proofs provide the required evidence that a proposition holds, thus an authorization request is permitted. In order to encode the proofs, proof terms are introduced (via Curry-Howard). Proof terms are sent between parties as representations of proofs of the validity of authorization requests, but they are not considered programs.

> **Comments:**
> **username_4**: You should mention dependently typed languages, as in them the line between proofs and propositions gets  blurred.  
> **username_3**: Indeed. Let's not forget Coq's program synthesis/extraction.  
> **username_5**: what program would correspond to a non-constructive (classical) proof of the form $\forall k \ T(e,k) \lor \lnot \forall k \ T(e,k)$? (Assume that $T$ is some interesting decidable relation e.g. $e$-th TM halts in $k$ steps.) (I can ask it as a new question if the answer is not very short.)  
> **username_6**: @username_5: do ask this as a separate question. In a comment you can say "the Godel-Gentzen translation is a continuation-passing transformation" but anything less cryptic won't fit. :)  
> **username_5**: @Neel, done: http://cstheory.stackexchange.com/q/5245/186  

---

### Answer by username_7 on 2011-03-02. Score: 10

In Coq, there are 2 types (Prop and Set), they are used by the programmer to separate what are proofs that won't produce actual code and the part of the proof that will be used to extract running code (your program).

That is a nice solution for the problem you ask about, how to identify what is meant to generate machine code (program) and what is present to complete the proof of the proposition (or type).

AFAIK there is no automatic way to distinguish both. This might be something interesting for research? Or maybe someone is able to point out it's clearly impossible?

With dependent types not only there isn't a clear distinction between proofs and programs but also there isn't a distinction between programs and types!
The only distinction will be where the type(or program) appear, making it part of the "program" place or of the "type" place of a given term.

An example will make it clearer i hope:

When you use the identity function with dependent types you need to pass the type your are going to use the function with! The type is being used as a value in your "program"!

Untyped Lambda Calculus:

id = $\lambda{x}.x$

With Dependent Types:

id : (A : Set) -> A -> A

id = $(\lambda{A}.(\lambda{x}.x))$

If you are using this function, then you would do it like this example:

id Naturals 1

Notice that the "type" (in this case the Set of Naturals) being passed as a value is thrown away so it will never be computed, but still it's in the "program" part of the term. That's what also will happen with the "proof" parts, they need to be there for the term to type-check but during computation they will be thrown away.


---

### Answer by username_8 on 2011-03-02. Score: 7

I will go out on a limb here and say that, if you are willing to squint a bit, proofs and **terminating** programs can be identified.

Any terminating program is a proof that you can take its input and produce its output. This is a very basic kind of proof of implication.

Of course, to make this implication carry information more meaningful than stating the obvious, you need to be able to show that the program works for any and all instances of input drawn form some class with logical meaning. (And so too for the output.)

From the other direction, any proof with finite inference steps is a symbolic program manipulating objects in some logical system. (If we don't worry too much about what the logical symbols and rules mean computationally.)

Types and propositions can be made to work similarly. Any type T can be assigned the proposition $\exists x : x \vdash T$ with obvious truth conditions. Any proposition can be turned into the type of it's proofs.

This is pretty simplistic, but I think it does suggest the robustness of the idea. (Even if some people are bound not to like it. ;-) )

> **Comments:**
> **username_9**: very good answer.  
> **username_10**: One should assume, of course, that you mean **finite** proofs and terminating programs. Some classes of non-terminating programs work just fine as infinite proofs. It's the non-productive non-terminating programs you need to watch out for.  
> **username_8**: I think this is a bit tricky, depending on how you are defining finite and infinite with respect to proofs.  In general, all proofs that we accept are finite, because they have to convince a human in a small finite amount of time.  A proof that relies on an induction scheme (i.e. most "infinite" proofs) are by this measure still finite, they just have symbolic steps that represent an infinite but regular computation.  A truly infinite proof, that I think most of us would reject as a valid proof, would be one where you literally had to consider an infinite number of distinct facts to validate.  

---

### Answer by username_2 on 2011-02-28. Score: 5

Proof irrelevance?

When you write some program, you are interested in its performance, memory consumption etc.  
E.g it's better to use some clever sorting algorithm instead of bubble sort, even if their implementations have same types (even in dependent type setting).

But when you prove some theorem it is only existence of a proof you are interested in.

Of course, from aesthetic point of view, some proofs are more simple/beautiful/inspiring/etc (e.g. proofs from The Book).


---

### Answer by username_10 on 2011-03-05. Score: 4

If you accept the Curry–Howard correspondence then the question is mainly a philosophical one. "Are proofs and programs different? Of course. How? Well, we call proofs 'proofs' and we call programs 'programs'."

Or to put it less flippantly, if there's an isomorphism between proofs and programs —which it seems clearly there is— then your question is asking whether there is any oracle capable of distinguishing the two. Humans categorize them as being different (for the most part), so it's certainly arguable that such an oracle exists. The important question then becomes whether there is any *meaningful* difference between them, which is up for philosophical debate. What is a "proof"? There is no formal definition of what constitutes a proof; it's a term of art, much like the notion of "effectively calculable" in the Church–Turing thesis. For that matter, "program" has no formal definition either.

These are words of natural language used to categorize different fields of mathematical enquiry. What Curry and Howard observed is that these two different fields where in fact studying the same thing. Noticing this connection is important because it says that these different researchers should be talking to one another. But on another level, to notice the connection is to belie the difference between them. When tackling a problem, sometimes it is more beneficial to think of it as a programming problem, whereas other times it is more beneficial to think of it as a logical problem. This difference in perspective is, I think, the important difference between them. But whether a difference of perspective constitutes a difference of identity is a deep philosophical question which has been explored at least as far back as Frege's *Ueber Sinn und Bedeutung*.


---

