|
|
|
|
|
by JohnStrange
3095 days ago
|
|
It's not just that, people spend way more time going through mathematical proofs, finding, and formulating them. If you give programmers time to muse about every function for weeks and write no more than 50-100 pages of program text per year or even less, then their programs will be almost bug free. You get what you pay for. Note: I'm not claiming that programmers should be treated like mathematicians or vice versa, I'm merely pointing out the differences of the activities. Edit: There is of course also a more trivial reason. On average, research mathematicians are probably more intelligent, skillful and diligent than typical programmers. |
|
Given the examples in the linked discussion of cases where not only did mathematicians write buggy proofs but it took years to figure out a mistake existed at all, let alone what it was, I find it hard to believe that. To the extent it may appear superficially to be true it's likely the result of the academic setting in which there is no connection to real world relevance and the only pressure that exists to get things done comes from peers and the need to publish papers - but if those papers achieve very little and your peers papers also achieve little, that's totally OK.
Compare to the world of the working programmer who is judged not by how fast he writes code but by the real world positive impact of that code, and it is easy to see how the mathematician may come across as more diligent or intelligent. But it's just an artifact of the pressure-free environment.
I was also surprised to learn that the idea of checking mathematical proofs using Coq is considered just as exotic or impractical as checking programs. I had thought that Coq and other proof assistants were in wide usage for this use case, as surely pure mathematics is simpler to reason about formally than entire programs ... but apparently not. The fact that maths proofs are still mostly checked by hand, whereas machine-checked proofs (like static type systems) are widely used by even novice programmers, is hardly reassuring.