It is not sufficient merely to prove a program correct; you have to test it too. Moreover, to be really certain that a program is correct, you have to test it for all possible input values, but this is seldom feasible.
This statement is tantamount to saying "you don't merely need to prove Fermat's Last Theorem, you also have to test it for all possible input values". By this line of reasoning, most of mathematics should be thrown out.
If you've proven a program correct, it is correct for all input values, whether you have tested them or not. If your proof ignores complexities such as the range of data values, it isn't a correct proof to begin with. And yes, proving programs correct is often possible -- in fact, the highest levels of software verification actually require explicit proofs of correctness for much of the code; see http://en.wikipedia.org/wiki/Evaluation_Assurance_Level#EAL7...
Mathematics sits atop a very small set of trusted axioms. Computer hardware is not so reliable; the parts are made in China as cheaply as possible. So even if you've proven something correct in theory, it doesn't matter because of all the additional variables that the real world introduces.
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.)
Actually most bugs are being introduced in the translation between pseudocode and your working programming language. For instance pseudocode does not deal with 32-bit integers that can overflow.
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.
Upvoted for the first two paragraphs, but I can't make sense of the second sentence of the third paragraph. The algorithm given in the article works in Python because Python has different overflow behavior than Java, C, or C++. When you say you "see no evidence", it seems like you are saying the implementation given in the article does work in Java etc.
> But in practice, it's easy to make a simple mistake in implementation and accidentally throw your proof out the window.
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.
It seems like you can only prove something in computer software up to the point of some random failure in hardware. If there's a chance that a cosmic ray will randomly flip a bit in memory every quintillion clock cycles, then surely you can only prove that an algorithm is correct with the explicit concession that it might be wrong every decade or so.
> This statement is tantamount to saying "you don't merely need to prove Fermat's Last Theorem, you also have to test it for all possible input values". By this line of reasoning, most of mathematics should be thrown out.
> 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 are making a categorical error: One proves algorithms and tests programs.
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 programs that can be proven are severely limited in power. For one, the tools to prove correctness of programs can't deal with data other than integers[1].
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.
Yes, and their practical usefulness is still severely limited.
[1] Of course, in theory this means they can deal with any data; in practice it means they can't.
For one, the tools to prove correctness of programs can't deal with data other than integers.
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?
For performance reasons. The SPIN model checker, which is the state of the art in terms of performance, employs only integers.
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.
you can prove theoretical programs. do you really want to have to prove that it still works with any random bit flipped at runtime? what about two random flipped bits?
All proofs start from some assumptions. When you are proving programs, you assume that the hardware is functioning properly. After all, anyone going to the expense of proving their software is correct will also pay for ECC throughout their hardware. Once you've proven your software correct, you can make assurances about the behavior of the software when run on particular hardware, and those assurances will be limited primarily by the reliability of the hardware.
You're challenging what it means for something to be a proof, which I think is always subject to philosophical debate. Intuitively, something is a proof of a proposition if it convinces someone else that the proposition is true, and the proposition actually is true.
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,
You can prove the correctness of a program given a specification of the language you write it in. But is the compiler you use to compile your program correct? Do you know all processor bugs?
I have heard from someone involved with project management of military aircraft software that the process includes verification of machine code produced by the compiler, that is: you have to prove that the code generated is exactly what you intended to get.
I have never seen a piece of software that is built with memory error tolerance is tested against random memory errors. Have you?
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.
They are a lot more common than you might think, basicly every day every PC has a memory error. If one of the textures in a video game gets corrupted you may not notice it, and if you have real issues simply rebooting tends to work well. Recent tests give widely varying error rates with over 7 orders of magnitude difference, ranging from 10^−10 to 10^17 error/bit·h, roughly one bit error, per hour, per gigabyte of memory to one bit error, per century, per gigabyte of memory.[7][8][9]http://en.wikipedia.org/wiki/Dynamic_random-access_memory The biggest defence for a home user is simply the banial nature of most information stored in memory.
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 too might be intressted in the link I posted above. Its about building safe hardware (and software), but I don't think its completly safe to anykind of random bit-flips.
What you are talking about is the "trusted computing base". Prove every part of the basesystem your running on, this of course is a HUGE task, but there are people thinking and working on this.
How do you prove the proof is correct? And how do you prove that your mathematical representation correctly corresponds to the problem you are modeling?
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 proof is a sequence of extremely easy logical inference rules like if A=>B and A then B. You check the correctness of the proof by verifying that these rules are applied correctly. Obviously though, there is no way to prove that your mathematical model corresponds to reality. That is because mathematics is not concerned with reality.
What if you make a mistake in checking the proof? Sure, that may sound silly, but mistakes are the point at issue here.
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.
Proving theorems in mathematics plays a bit different role than proving correctness of programs. In mathematics, it's about sharing ideas, so if the proof is not completely correct, it can still be interesting because of the ideas and methods it uses. When you prove correctness of programs though, the whole point is to be sure that the program is correct, so the actual proof is important here, not its method or structure, because it's usually clear why the program at hand works.
If you make a mistake in checking the proof, the the proof is incorrect. The problem is with your application of the mathematics, not the applicability of mathematics itself to the problem of showing the truth of things.
It depends on the scope of the proof. It's sloppy to say "this is proved to be correct". They should say "this is proved to be terminate with output X in a finite time, for input values in the range -Y:Y".
Everything can be proved to be "correct", for some definition of "correct" (i.e. "output undefined, program may not terminate").
This statement is tantamount to saying "you don't merely need to prove Fermat's Last Theorem, you also have to test it for all possible input values". By this line of reasoning, most of mathematics should be thrown out.
If you've proven a program correct, it is correct for all input values, whether you have tested them or not. If your proof ignores complexities such as the range of data values, it isn't a correct proof to begin with. And yes, proving programs correct is often possible -- in fact, the highest levels of software verification actually require explicit proofs of correctness for much of the code; see http://en.wikipedia.org/wiki/Evaluation_Assurance_Level#EAL7...