3 ms·
Interesting argument, though I currently think correctness is more important in programming. Their proofs are hand-wavy compared to our programs. Thurston expa
by calibraxis 13y ago
Interesting argument, though I currently think correctness is more important in programming. Their proofs are hand-wavy compared to our programs.
Thurston expands, "It’s just that the reliability does not primarily come from mathematicians formally checking formal arguments; it comes from mathematicians thinking carefully and critically about mathematical ideas." (http://arxiv.org/abs/math/9404236 http://arxiv.org/abs/math/9404236)
But I could also accept the claim that mathematics is more intellectually gratifying, if they're not so much at the mercy of standardization and other boring fiddly issues. I don't know.
- pseut 13y agoI disagree. A small nearly impossible to encounter edge case error may or may not be worth fixing in a program, but it invalidates a proof.
- hyperpape 13y agoDepends. Many proofs have errors in them. You'll only get people to pay attention if it's difficult/impossible to repair those errors for a reasonable practitioner. In contrast, since a program is executed by a computer, many sorts of errors will cascade. I think the right thing to say is that a proof must be 100% conceptually sound. But a program relies on many many more bookkeeping details that must be correct or there will be bad behavior.
- Mindless2112 13y ago> Interesting argument, though I currently think correctness is more important in programming. Their proofs are hand-wavy compared to our programs. This is where proof systems like Coq come into play. You can write code in Coq and then use Coq to formally prove properties about it -- the CompCert C compiler [1], for example. Or you can model real-world problems in Coq and use Coq to help you prove them. Either way, proofs don't have to be hand-wavy. [1] http://compcert.inria.fr/doc/ http://compcert.inria.fr/doc/