go ahead... be a heretic  
PerlMonks 
Re: OT: Mathematics for programming (again)by tilly (Archbishop) 
on Sep 10, 2008 at 21:36 UTC ( #710474=note: print w/ replies, xml )  Need Help?? 
Ironically the proofs that professional mathematicians create are almost never truly rigorous either. The difference is that a mathematician knows how, in principle, they should be able to make it rigorous. Assuming that there are no errors. Which is often a dubious assumption. How do I explain it? Imagine that you wrote down a detailed outline for your computer program in pseudocode, but you never tried running it. Suppose you convinced yourself that the outline was complete and unambiguous. That's kind of like a mathematical proof. Suppose two other programmers were selected read your spec closely, agreed with your assessment, thought it was interesting, and didn't find any major mistakes. That's kind of like a published mathematical proof. Based on your experience programming, how many small, niggling problems do you think you'd encounter if you tried to turn that outline into a real program? How possible is it that you'd encounter something that would require a larger rethinking? Do you think you might encounter a fatal flaw that would make your program useless?
That's how math is. Lots of proofs have errors. It has happened (for instance to an Italian school of geometry in the late 1800s) that there have been entire areas of mathematics that collapsed under the weight of accumulated Just waving a mathematical wand and saying we have a proof doesn't mean that we're right. That's not to say that trying to construct proofs about our programs is not a worthwhile exercise. But it isn't a magic cure either. Edit: planetscape noticed that I said areas instead of errors. I found this very ironic, but fixed it anyways.
In Section
Meditations

