> Interesting argument, though I currently think correctness is more important in programming. Their proofs are hand-wavy compared to our programs. This is whe

> 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/