3 ms·
Because he argues under the same incorrect assumption that writing mathematical proofs is more fault-proof than writing code. Which is what the answers on stack
by zzzcpan 9y ago
Because he argues under the same incorrect assumption that writing mathematical proofs is more fault-proof than writing code. Which is what the answers on stackexchange are partly about.
- moocowtruck 9y agoi think he's arguing that it gives us a more precise language to describe our documentation than just regular comments, not that mathematical proofs are fault proof
- posterboy 9y agoI liked this part of one answer especially > Still, I hope that this sheds some light on the question that is implied: "What really is the difference between proving some theorem and writing a program?" (To which a careless observer of the Curry-Howard correspondence might say: "Nothing at all!")