In my opinion, many people are curry Howard blind. It's like they found this one correspondence between certain proofs (constructive ones) and programs and are hell-bend on using it. Personally I like not to confuse the two things. Proofs are proofs, programs are programs, programs can generate proofs, proofs can verify programs. And proofs are classical.

Identifying proofs with programs undeniably gives a beautiful economy of concepts, best experienced among mature tools maybe in Agda.

But there is a price to be paid, and that's the restriction to constructive logic. If you need classical logic, use an LCF-style prover like Isabelle/HOL.

> But there is a price to be paid, and that's the restriction to constructive logic.

That's the price on the proof side. The price on the program side is the need to encode complexity in the types because C-H is about abstract programs, not computations.

Otherwise, the existence of a computation is entirely ignored except where it may break the logic's consistency in the case of non-termination, but from the computation's perspective, a long computation and a non-terminating one are the same. The result is that you can "prove" the correctness of programs that are effectively non-computable, i.e. programs that don't encode effective computations (by effective computation I mean one that terminates before the end of the universe, but it could be exchanged with more practical definitions).

Yeah, I agree that it should be routinely called the C-H correspondence.

What's a suitable resource depends on your background. If you like books, "Proofs and Types" by Girard, Lafont, Taylor [1] is a great read, albeit idiosyncratic.

[1] http://www.paultaylor.eu/stable/prot.pdf