Proofs are not programs

The Curry-Howard correspondence can be pithily described as saying “proofs = programs”. The statement is short, alliterative, and rather beautiful. As a professional mathematician I know exactly what a proof is; as an amateur programmer I have a pretty clear idea about what a program is, and the concept that they might be in some sense the same thing is both enigmatic and appealing. A proof is a logical sequence of statements deducing a theorem from the the rules of maths; a program is a logical sequence of commands producing valid code from the rules of the programming language being used. When learning Lean I saw the correspondence in action many times, and so it actually took quite some time for the penny to drop: the Curry-Howard correspondence is not actually true.

Of course something is true, but what is not true is any statement of this form where “proof” is interpreted as “what the pure mathematicians in my department do”. What is true is that if you stick to constructive maths or intuitionistic logic or one of the flavours of maths where you’re not allowed to use the axiom of choice or the law of the excluded middle — in other words a version of maths which is unrecognisable to over 95% of pure mathematicians working in mathematics departments — then you might be in good shape. But that is not what I see happening in my mathematics department or the other mathematics departments which I’ve had experience of. Some proofs are not programs.

Here’s an example of a proof which is not a program. The original proof that the class numbers of imaginary quadratic fields tended to infinity was the following rather extraordinary argument. First Landau showed that the theorem was true assuming that a certain generalisation of the Riemann Hypothesis was true, and then Heilbronn managed to show that the theorem was true assuming that this generalisation was false! See for example Keith Conrad’s comment on this mathoverflow question, and for more details see p359 of the book “A Classical Introduction to Modern Number Theory” by Ireland and Rosen (I have a copy of this book in my office if any Imperial students are interested in seeing more details).

The analogous situation for programs would be something like the following. Your boss asks you to write some computer code to do a certain task so your company can release their new product. A week later you enter their office with two USB sticks, explaining that one of them does the task if the Riemann hypothesis is true, and the other one does the task if the Riemann hypothesis is false. What you seem to have done, on the face of it, is proved that the code your boss wanted exists. You might also have lost your programming job 😉 In fact it’s not even 100% clear that you have proved that the code exists — what if we replace the Riemann Hypothesis in this story by one of these weird unprovable logic statements like the continuum hypothesis, which is true in some models of maths and false in others? Then where’s the program?

But actually it’s even worse than that. In my last blog post, I gave an example of a computable bijective function which did not have a computable inverse. A similar sort of argument shows that the following proof:

Theorem. If is a surjective function, then there exists a map such that is the identity function.

Proof. Define thus: if then choose with (possible by surjectivity of ) and define to be this . The fact that is true by definition. QED.

does not correspond to a program. The theorem is just the axiom of choice in disguise, and the axiom of choice is about as non-constructive as you can get. Programs are algorithms. The axiom of choice says that we can do something when there is no algorithm.

What is a Lean file then?

So this a bit confusing, because I can prove that theorem above in Lean:

noncomputable def g {X Y : Type} {f : X → Y} (hf : function.surjective f)
  (y : Y) : X := classical.some (hf y)

lemma g_prop {X Y : Type} {f : X → Y} (hf : function.surjective f) 
  (y : Y) : f (g hf y) = y := classical.some_spec (hf y)

theorem has_right_inverse_of_surjective (X Y : Type) (f : X → Y)
  (hf : function.surjective f) :
  ∃ g : Y → X, ∀ y : Y, f (g y) = y := ⟨g hf, g_prop hf⟩

and that looks like code to me. But not all computer files are computer programs. As an example, consider a LaTeX file. The LaTeX program is the program, the LaTeX file is just the input to the program, and the output is typically a pdf file.

Lean itself is a program, but the Lean files which people make are not all programs. Some of them are though! Some Lean files (which use constructive logic and only computable functions) are turned into bytecode when run through Lean, and bytecode is a program. But no bytecode is generated for the definition of the function g above because it is noncomputable, and that stops the proof has_right_inverse_of_surjective from ever being a program. Lean itself can verify that the proof is correct, but the proof itself is not a program.

I am still getting to grips with all this computer science malarkey. I asked a bunch of questions about this stuff when writing this blog post, on this thread in the Lean chat (login required), and thanks as ever to Mario Carneiro for answering most of them.