9 ms·

Is there some better resource for learning programs-are-proofs people should be using?

auggierose 11y ago
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.
- mafribe 11y ago
  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.
  - pron 11y ago
    > 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).
- tel 11y ago
  Yeah, I agree that it should be routinely called the C-H correspondence.
mafribe 11y ago
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 http://www.paultaylor.eu/stable/prot.pdf

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.

mafribe 11y ago
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.
- pron 11y ago
  > 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).
tel 11y ago
Yeah, I agree that it should be routinely called the C-H correspondence.

mafribe 11y ago

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 http://www.paultaylor.eu/stable/prot.pdf