I\'ve been studying constructive type theory (CTT) and one of the things that I\

Question

I've been studying constructive type theory (CTT) and one of the things that I'm not clear on is the proof part: Proving the correctness of a program in a form of a proof that's nothing but the program itself (Curry-Howard Correspondence)

Most examples that I've seen in books (e.g., Type Theory and Functional Programming - Thomson and TaPL) show the "proofs" on ?-abstractions and applications on terms (i.e., literally a,b,e...). The proofs seem to mostly rely on the type signatures of the functions, under the assumption that the function does what it claims. Not much is discussed about the "how" of the function's correctness.

For example, when writing a real program (e.g., in Haskell and other [pure] functional languages), the function under consideration could do any arbitrary computation and return a term of the correct type for the proof to go through (statically speaking). So how do we know that the program is computationally doing the "right" thing (dynamically speaking) and not just faking it to get past a proofing system?

From what I understand, here's how things should go (and probably are, but I'm not sure if I'm right), crudely speaking:

Given a program's specification in something like predicate logic we "convert" it into an equivalent "typed representation"
Using backward inference we substitute the "functions" with their appropriate values, which themselves could be other functions (i.e., we replace the functions with their computation rules, but I'm thinking more on the lines of replacing the function with its body, from a programming point of view, for the sake of argument. Assuming that they're "returning" the correct type this seems like a believable substitution)
We continue doing #2 above till we hit primitive operations (again, crudely speaking) which we can trivially prove (or if not, maybe the proof is "simple" enough).
Once we've hit all the "axioms" (or trivial proofs) along all the branches of backward inferences, we stop.
QED

Two questions:

Is my understanding/intuition of "how" the proof of correctness works in CTT works correct? It looks like it won't be possible for the program to "cheat" this or can it?
And secondly, is this what proof assistants like Coq help you prove/analyze (at a high level)?

Explanation / Answer

Proving the correctness of a program in a form of a proof that's nothing but the program itself

This is not quite how the Curry-Howard-Correspondence works.

First one has to show that the language of choice actually corresponds to some consistent logic. Different languages correspond to different logics, and many languages correspond to inconsistent logics which are not good for proving things. Haskell doesn't correspond to a consistent logic, because in Haskell, we can write nonterminating programs which would correspond to infinite proofs. But infinite proofs are invalid, so not every Haskell program corresponds to a valid proof.

Now what does it mean that a language corresponds to a logic? It means that:

a type in the language corresponds to a formula in the logic
a program in the language corresponds to a description of a proof in the logic
a well-typed program in the language corresponds to a description of a valid proof in the logic.
a program of a specific type in the language corresponds to a proof of a specific formula in the logic
a value in the language correspond to truth in the logic
evaluation of programs to values corresponds to soundness of the proving rules
reification of values to programs corresponds to completeness of the proving rules
...

No need to understand all aspects of the correspondence at once, but it is good to keep in mind that the correspondence relates not just programs and proofs, but many (all?) aspects of the languages and the logic. For the question here, only the first four aspects are relevant.

A minor issue is that only well-typed programs correspond to valid proofs. That's why type signatures of functions are so relevant to the Curry-Howard-Correspondence.

The key issue is that a well-typed program doesn't correspond to a valid proof of its own correctness, but to a valid proof of whatever formula corresponds to the program's type.

For example, let us consider the following two programs (using Haskell syntax, but assuming a version of Haskell that corresponds to a consistent logic):

f :: a -> a -> a
f x y = x

g :: a -> a -> a
g x y = y

The functions f and g are well-typed programs of the same type, so they correspond to valid proofs of the same formula. The formula is "forall propositions p, p implies that p implies p".

But clearly, f and g are different programs. And of course, they correspond to different proofs of the same formula. The program f corresponds to the proof "We know that p implies p, so also p implies (whatever implies p)". And the program g corresponds to the proof "We know that p implies p, so also whatever implies (p implies p)."

Usually, with programming languages, we care about the difference between programs like f and g, and with logics, we don't care about the difference between the two proofs that correspond to f and g. But when thinking about the Curry-Howard-Correspondence, it is important not to forget that there can be multiple different valid proofs of the same formula.

So how do we know that the program is computationally doing the "right" thing (dynamically speaking) and not just faking it to get past a proofing system?

We don't. We only know that the program proves the formula we have encoded in the program's type. So how can we use the Curry-Howard-Correspondence to prove a program correct? We have to encode a statement about program correctness into the type of the program. This requires a very expressive type system, of course, which is exactly what the languages inside tools like Coq or Agda provide.

Related Questions

Navigate

• Browse (All)
• Browse I
• Subjects

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.