Re: "Math is hard"
I was addressing the one part of the problem which programmers can address--their own code.
The hard part of applying proofs to the real world is uncovering the assumptions that are being made. That is the critical aspect of a mathematician's training, and the difference between what one will accept as a theorem and what will scooch past someone else. Your comment does a nice job of uncovering what is needed for a complete claim of correctness.
However, I specifically did not bring in formal checking. Formal tools are always going to lag in capabilities, and, in the hands of people who are not mathematicians, are readily abused.
Biting the hand that feeds IT
