Re^2: OT: Mathematics for programming (again)

[vrk]

Another example is the proof of Fermat's last theorem by Andrew Wiles. Since the proof is long and involved, it took the author himself to point out the errors, and later fix them.

I take it you are advocating that the only good way to ensure a program is correct is to run it on a computer. But here's an inherent problem: your mental model of the semantics of the programming language you use and what is actually implemented on the computer are bound to differ. Which one is correct is subject to debate (i.e. whether the documentation -- which is the only thing consumable by humans -- or the implementation -- which is consumable by computers -- is definitive). A document may be ambiguous, yet a human reading it can still understand what is meant. A computer program cannot be unambiguous. What may happen is that you interpret the program differently from the computer.

A further problem is the level of explicitness required. Machines do not have creative thinking, so every last little detail has to be spelled out. Humans, on the other hand, can guess, find connections, and derive on existing knowledge when interpreting a document. Excessive detail will only hamper understanding, which is directly contrary to computer programs. A computer will make all idiot mistakes you never thought anyone reviewing the program would.

[tilly]

I'm not advocating that the only good way to ensure a program is correct is to run it on a computer. However I am saying that actually running it on a computer tends to catch a lot of things you don't catch otherwise. Furthermore when you add in unit tests, QA, and other best practices that can only happen after the code can be run, you catch even more. Therefore a program that has only been desk checked should be viewed with suspicion.

As for why mathematicians don't do this, you've hit on some of the reasons. Mathematicians only seek to convince other mathematicians of their results. They strive to be critical of themselves and others, but at the end of the day if you can convince other mathematicians that you have a proof, that's what matters. Therefore there is no need or desire to write proofs out in unreadable formal detail, but there is a need to clarify the central point in a way that other humans will understand.

[casiano]

The only good way to ensure a program is correct is to run it on a computer.

and viceversa (s/program/proof/g):

The only good way to ensure a proof is correct is to run it on a computer.

If not, what was the reason for all Turing/Godel/Church efforts to fix David Hilbert's problem question on the completeness and consistency of mathematical systems? (Hilbert's program)

That's one of the meanings of Knuth's famous quote

"Beware of bugs in the above code; I have only proved it correct, not tried"

A constructive proof that uses only finite procedures (algorithms) and runs in a Turing-equivalent machine has more value than an ordinary mathematical demonstration.