mbp, Thanks for your last couple of posts. I am reminded that Computer Science is much closer to Physics than Mathematics. Machines are bound by physical reality, and while mostly under our control, are subject to unexpected events which makes "proof" unattainable.

The mathematical proof, is still a useful techinique in eliminating most expected bugs. If we prove that a program computes the gcd, we can have little doubt of it's function on a real machine, assuming the input integers are within the machines limits.

raph, writes:

I believe that it is possible to design programming languages and runtimes to be much, much simpler.

It's already been done, it's called colorForth.

Compatibility with existing designs is also important. Internal consistency can be proved, but compatibility can only be tested. This principle extends to file formats, programming languages, instruction sets, compression algorithms, communication protocols, file systems, all manner of I/O techniques, API's, etc. In other words, most of the things you care about when building a real system.

GNU is faith based computing. There is no way any one person check all these things, not even close. You have trust the work of others to a high degree, and also make broad assumptions in creating new work.

--- Update

graydon, Actually that was a quote of raph. My apology for the confusion, my quotation style was ambiguous.