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)
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.
Depends. 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.
> 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.
However, the evolution of math often goes towards generalising a certain behaviour, operation or set.
For example, first we had the natural numbers and the addition operation. Then addition was generalised as an operation on different 'objects' like matrices, equations, etc
So, yes, the strong typing idea makes sense, maybe someday math will be able to generalise addiction for any set and any object based only on their properties, regardless of what they are.
If you want to see generalization look no further than Category Theory. But it's all done "safely": you define what a category is, and prove things about it, and then declare how certain objects can be viewed as categories (somewhat like the typeclass pattern).
