What is the difference between proofs and programs (or between propositions and types)?

Given that the Curry-Howard Correspondence is so widely spread/extended, is there any difference between proofs and programs (or between propositions and types)? Can we really identify them?


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 Adapting Proofs-as-programs pushes this angle with the aim of synthesising imperative programs. With dependent types becoming more and more popular, certainly in research functional languages (Agda, Epigram), the distinction is becoming blurrier. Of course you can do program synthesis/extraction within the Coq 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. 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.

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.

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. ;-) )

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

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.

Need Your Help

How to use Espresso Idling Resource

android android-testing android-espresso

The scenario is when the user click on the "Download" button, the data (a music/an image etc.) starts being downloaded from the internet. When the download is finished, the button changes it label ...

How to send email by using MailKit?

c# gmail mailkit

According to the new google politics https://googleonlinesecurity.blogspot.de/2014/04/new-security-measures-will-affect-older.html I can't sent an email. "Less secure apps" are considered for googl...