(original title: "Curry Howard is a scam". See below.)

The Curry-Howard correspondence has been talked about a lot recently, not only in Haskell circles, but also among CiC-based proof assistant practitioners (Coq, Lean, etc.). In a nutshell, it makes a deep parallel between "programs" (terms of some flavor of lambda calculus, typically), and "proofs" (these programs are a proof of their type, or more precisely they are witnesses that their types are inhabited). The most basic example is id x = x which, in Haskell, would be a proof of $ \forall a. a \rightarrow a $, a trivial theorem of propositional logic.

That's all good and well, but my point here is that in practice, the equivalence is not as interesting as it first looks.

Programs are not really proofs

A real program (i.e. one that is written to be executed and do something useful) is not really a proof of anything interesting. Pedantically, a haskell program has type IO (), which is not really a valid proposition. But even beyond that, if we look just below the surface of main, nothing has that interesting a type:

A classic Haskell program that is used by people is pandoc. Most of what it does could be described as Doc Markdown -> Doc Html (or a similar pair of document formats). So you have a "proof" that these two trees can be somehow mapped onto one another. No mathematician will fawn over that.

Servers written in Haskell, like webservers, would have the type request -> IO response (or something close to that, maybe request -> M response for some custom monad M) if you look inside the server loop. Again that's not really mathematically interesting.

It's only if you look in combinator libraries (like Parsec, say) that types get more generic, and start looking more like formulas. Things like flip : (a -> b -> c) -> b -> a -> c are as generic as it gets… and are proofs of super trivial propositional logic theorems. In fact you can't even state much in Haskell, any real mathematical statement will at least require first-order logic (which corresponds to dependent types — no mainstream language features these beyond, er, C++). Idris could possibly have some interesting proofs that are also real programs… if it were designed to be a proof assistant and not a beefed-up programming language.

If anyone has a useful program that is also actually a proof of something non trivial, I'd be happy to be proven wrong.

Proofs are not really programs

What is the program corresponding to a proof of "there exists an infinite number of primes"? If I run this program, what input does it takes, and what do I get as an output?

I don't have a direct answer to that question. If you develop this proof in Coq, using a Prop typed statement, I don't even think it could be extracted to OCaml and compiled.

For most of mathematics, I have no idea what the "programs" corresponding to proofs found in textbooks would look like, nor what they would compute. There are very complicated lambda terms for these proofs, but what they compute is unclear.

A concession

A domain where CH does make sense to me, is algorithms (written in a functional style) that are used as existential witnesses of some property. For example, the Euclid GCD algorithm is, in a very real sense, a proof that two natural numbers have a GCD. You can write some Coq or Lean code that computes the GCD of two numbers and proves that it's indeed their greatest divisor.

That said, I don't know of any large program written this way. It's a labor intensive way of writing programs, even compared to alternatives like why3 where you can cleanly separate the code and the specification, and ask automatic provers to do as much proving as possible for you.

But what about Compcert/SEL4/… ?

Let's look at Compcert, famously one of the largest programs written in Coq. I suppose the main type is compile : C_program -> Option Asm_program or something like that (I'm no expert on Compcert so I could be very wrong). However, as far as I know, it's not written in a purely dependent style: proofs are separated from the "real code" part of the development. This means we don't get $\forall x: \text{C_program} \rightarrow Option \set{y : \text{ASM_program} | R(x,y) }$ where $R(x,y)$ would mean that $x$ and $y$ have the same semantics; rather you have C_program -> ASM_program and proofs on the side that the function preserves its input's semantic.

For SEL4 it's developed with Isabelle/HOL, which isn't dependently typed and is classical logic.

Conclusion

The title was click-baity, of course 🙂. But I do think that CH is over-hyped, because the correspondence is only mostly interesting abstractly; in practice things are either a (interesting) program, or a (interesting) proof, but not both at the same time.

edit (2021-02-24): I regret the over-aggressive title now. Changing it to the more appropriate "CH is overrated"; it's obviously still a useful mathematical statement and a valid way of building proofs.