The big insights in computer science look very much like mathematics; the mechanics of a binary search work perfectly in theory. But in practice, it's easy to make a simple mistake in implementation and accidentally throw your proof out the window. The proof remains valid, but your implementation isn't doing what the proof says.

The fact that a famous book on proving correct and then implementing a binary search ended up being slightly wrong underscores how easy it is to make this mistake. (I find binary search a little annoying because of the integer division. Do you round up or round down? What does your language implementation do? Now you see why you need to mentally prove that you've written the right algorithm, and then test to make sure your computer is doing what you think you're telling it to.)

But that's not the fault of the algorithm, or the fault of its proof and it also has nothing to do with the origin of your computer parts.

Also, the "mechanics" of binary search work perfectly in practice. I see no evidence to the contrary, either in your comment or in the above article and that same implementation described works perfectly in Python.

But that's not how a proof of correctness works. You have an implementation (of an algorithm, say) and you prove mathematically that it is correct with respect to a formal specification. The implementation and proof aren't separate things.

   — Donald Knuth

> If you've proven a program correct ..

You are making a categorical error: One proves algorithms and tests programs. A program is a representation of an algorithm. If the language of implementation e.g. Haskell is purely functional, and your representation e.g. data types is faithful to the algorithm, then you can make claims about your provably correct implementation.

You can prove programs too, not just algorithms. That's what the entire (exorbitantly expensive) field of verified applications lies upon. Even my college class on formal logic covered the basics of this, and there's billions of dollars worth of extremely high-reliability applications that have been developed using such formal proofs.

For example, Green Hills Software's INTEGRITY operating system has bounds on the runtime and behavior of system calls formally verified, so one can reasonably guarantee that a malicious user cannot DDOS the system by making system calls with unbounded duration.

There are even entire programming languages designed for the sole purpose of making formal, mathematical verification of programs easier.

A program is a representation of an algorithm.

Yes, which is why you have to prove it correct again, since real programming languages, e.g. C, have limitations not typically present in the original algorithm.

The way this usually works is that the proof is written and the code is then generated from the proof. That code is then incorporated in something larger, which has not been proven correct. Such is the case with algorithms. You can mathematically prove an algorithm correct. You can even write a proof and generate a program from it. Then you still have to use that algorithm and all the code using it can't be proven correct with current methods. That is why you will still have to test your program.

  There are even entire programming languages designed for
  the sole purpose of making formal, mathematical
  verification of programs easier.

[1] Of course, in theory this means they can deal with any data; in practice it means they can't.

This is the first time I hear such claim. Which tools are you talking about? The tools I know (Coq) certainly don't have such limitations -- why would they, anyway?

Has Coq ever been used to solve an actual practical industrial or business problem, either by generating code from a known correct program or by using the Coq model as an oracle to drive automatic testing? If not, then there's your answer: academically useful proof assistants cannot deal with real world data. Proof assistants useful in the real world can only deal with limited data types to be able to achieve their goal.

Obviously, for difficult concepts, it's possible that every expert in the world could be convinced that a proposed proof is correct, only to later find out that it's not. The way I see it, you're always only proving that something has a high probability of being correct, and showing how high the probability is. For computer software, you might be showing that your program is correct with the same probability that the underlying hardware is working as specified (so cosmic rays shifting bits or faulty hardware are possible exceptions baked into your proof).

To get a bit silly, a mathematical proof delivered from person A to person B is really only showing that a proposition is true with the same probability that person B is sane, educated, and is understanding the concepts correctly,

Do you think testing (likely on a different machine than the target) will catch a 1 in a million hardware error either?

http://www.sandroid.org/birdsproject/4dummies.html gives a glimpse of how much fun developing software for aviation purposes is.

Rule 1: you can't trust RAM it lies.

That said you can build automated tests that add random memory errors to help find the program that's best able to handle memory errors.

Maybe a spacecraft might have some. Error correcting memory, and the software associated with it is, of course, an exception. Is there code dealing with memory errors somewhere in the kernel (of any OS)?

For most programming, it would simply not make sense to try to take memory errors into account. It's very unlikely that in the lifetime of the program, there will ever be a situation where a bit will be flipped and it will have an actual effect.

Yet, you don't have to be building a spacecraft for rebooting to be an issue. One example that comes to mind is remote sensors. A friend was working on power meter which reported back it's findings every few days. The initial version used normal programming practices and after a six months field test of a few thousand units the projected failure rate over 10 years in the field was unacceptably high. He said the code was simple and 'correct' but failed to deal with with corruption. His version had less than 1% of the original failure rate in the field and is projected to save the company far more than his 6 month contract to rewrite the thing from scratch.

A more dramatic example is your car's internal engine controls. But, there they simply reboot regularly as there is no need for maintaining state over the long term.

You might injoy this darpa project: http://www.crash-safe.org/papers

The propose there own hardware, OS, languages and compilers. The Hardware Design is by Tom Knight, one of the guys who designed the lisp machine.

Its quite an intressting read.

This is why I am bitter and disillusioned about mathematics: it promises certainty, but doesn't deliver. It remains pragmatically useful, like many other tools, but does not deserve the semi-mystical status some confer on it. </rant>

The usual rejoinder is that you can use an automated proof checker/assistant like COQ. Now you're relying on a program. Is the program correct? Well, we checked it with itself...

I admit this is far better than not having a proof at all. As I said, it's a tool, and has pragmatic merit. My objection is it's not absolute proof - which is what "proof" sounds like to me. In reality, a proof is an argument for the truth of a claim, with a level of convincingness.

BTW: Admittedly, reducing a proof to simple rules makes it harder to get wrong, though this is rarely done by mathematicians. Also, it's a curious fact that some mathematicians have made mistakes in their proofs, but turned out to be right anyway, presumably because they could see that it was true, and the notation was secondary.

Everything can be proved to be "correct", for some definition of "correct" (i.e. "output undefined, program may not terminate").