I agree with you that if you want to prove the correctness of a new algorithm, you need to prove the correctness of that new algorithm. You're gonna want some

I agree with you that if you want to prove the correctness of a new algorithm, you need to prove the correctness of that new algorithm. You're gonna want some proving skills there. How often are programmers developing new algorithms? I guess it depends on where you draw the line for "algorithm", but let me propose two possible places for the line. On the one hand, you might use existing techniques in a new function. In this case, the proving technique you need is the theory of invariants and so on, as Dijkstra ranted about. You're not gonna need a lot of practice with higher-level math proofs for that. That's even assuming you care about "proving that it does what you say it does in all possible cases", which of course we all know is done by roughly 0% of programmers, especially with emphasis on the "in all possible". On the other hand, you might make a bigger development, that requires more mathematical expertise. I suggest for your consideration that the correct description of a person doing this latter work is not "programmer", but "professor" (or grad student), and that this is relatively rare, and if this is what you meant all along, you've been using misleading language. I think you have it absolutely backwards when you say "this is an extremely rare case"; I think the case where you need real mathematical proof techniques is the extremely rare case, even in relatively math-heavy areas, e.g. numeric simulation. What you need, as I've said before, are techniques of calculation. Also, my ML knowledge is weak, but from my modest knowledge, I don't think any of it works provably. It works probably. :) Seems a weird example to choose. At this point, btw, I acknowledge that I'm thoroughly into "quibble" territory. =]