Given the "programs as proofs" isomorphism, how do we know that the program isn't lying?

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 $\lambda$-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:

1. Given a program's specification in something like predicate logic we "convert" it into an equivalent "typed representation"
2. 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)
3. 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).
4. Once we've hit all the "axioms" (or trivial proofs) along all the branches of backward inferences, we stop.
5. 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)?

Answer 1

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.

Answer 2

In some sense it doesn't matter what the function does, as long as it takes the correct types and produces something of the correct type. The trick is that when you start talking about the Curry-Howard correspondence, the types are much more precise and specified that what we'd normally deal with day-to-day.

Moreover the Curry-Howard correspondence says that we can take a proof (in a variety of different logics) and produce a program by a "simple" substitution, and we can take a program (in something essentially lambda-calculus-esque) and produce a proof about the types.

So it doesn't quite say that it proves what the program does, it just proves a statement about the types. So a function that takes a natural number and produces a natural number is a proof that given a natural number, we can produce a natural number. It gives us nothing in particular (without extra work) about what number it actually produces.

When you start using more precise types, then things start to get interesting, and you get something like the process you outline, and give or take particulars, how things like Coq work.

To give an example from Coq, we can define a function:

Definition zero (n : nat) : nat := 0.

So all we get is zero, but if we look at the type of zero, we get nat -> nat. Not particularly interesting (but correct, which is what the type checker gives us).

We can however prove something about it:

Lemma zero_always : forall n, zero n = 0.
Proof.
  intros. destruct n. reflexivity. reflexivity.
Qed.

This is Coq's syntax for proving things, which gets translated into a program:

zero_always = 
fun n : nat =>
match n as n0 return (zero n0 = 0) with
| 0 => eq_refl
| S _ => eq_refl
end

So the proof is a function that destructs the nat type, and applies some other thing which says that things that look identical are the same. Now the type of zero_always is

forall n : nat, zero n = 0

Which is a function from nats (which we will give the label n) to things of type zero n = 0. So you can see that the types we need to say something useful about a program are a bit unusual compared to the run of the mill datatypes (but not really different in this context).

Going back a step, the eq_refl is actually a constructor of a type eq. eq has only the one contructor which is eq_refl : x = x where x : A, A: Type and hence eq : A -> Prop. Unravelling that, equality is a function that takes a single element of some type (for every type A) and produces a Prop (which is a proposition type, really just a Type but Coq uses it for convenience for other reasons) that says that element is equal to itself. So our zero_always proof applies a function that just applies another function, and because the very carefully chosen types match, we're happy (as long as we trust the type checker ;) ).