= 27d567bc2d48d9f40e9ccc20ea370b15)
abramdemski comments on Second-Order Logic: The Controversy - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (188)
I'm generally not on board with the whole "programs are proofs" dogma. When I look into the details, all it says is that a successful type-check of a program gives a proof of the existence of a program of that type. In expressively powerful languages, this seems very uninteresting; so far as I know, you can easily construct a program of any type by just discarding the input and then creating an output of the desired type. (Handling the empty type is a little tricky, but I wonder if infinite loops or program failures would do.) So my understanding is that you only get the interesting type structure (where it isn't trivial to prove the existence of a type) by restricting the language. (Typed lambda calculus is not Turing-complete.)
So, while I see the curry-howard stuff as beautiful math, I don't think it justifies the 'programs as proofs' mantra that many have taken up! I don't see the appeal.
If course this isn't quite true. Other interesting things which are said include the idea that a proof of a conjunction can be handled as a pair of proofs (one for each element of the conjunction), and a proof for a disjunction can be a proof for either side, and so on; so in a sufficiently rich type system, we can leverage the type machinery to do logic, using product types as conjunctions, sum types as disjunctions, and so on. A proposition is then modeled as a type for a proof. An implication is a function type, proven by a procedure which transforms a proof of one thing into a proof for another.
Still, I can't swallow "programs are proofs / propositions are types".