9 ms·

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 f

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:_Formally_Verified_Design_and_Tested http://en.wikipedia.org/wiki/Evaluation_Assurance_Level#EAL7...

Bootvis 15y ago
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?
- onemoreact 15y ago
  Computer hardware is not correct. So, you need to step past mathematical perfection and write defensively. 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.
  - nickik 15y ago
    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.
  - exDM69 15y ago
    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.
    - onemoreact 15y ago
      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 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.
- chokma 15y ago
  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. http://www.sandroid.org/birdsproject/4dummies.html http://www.sandroid.org/birdsproject/4dummies.html gives a glimpse of how much fun developing software for aviation purposes is.
- nickik 15y ago
  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. You might injoy this darpa project: http://www.crash-safe.org/papers 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.
torstein 15y ago
"Beware of bugs in the above code; I have only proved it correct, not tried it." — Donald Knuth
jrockway 15y ago
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.)
- bad_user 15y ago
  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.
  - arundelo 15y ago
    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.
    - nknight 15y ago
eternalban 15y ago
> 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.
- DarkShikari 15y ago
  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.
  - nazgulnarsil 15y ago
    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?
    - wtallis 15y ago
      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.
6ren 15y ago
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>
- adrianN 15y ago
  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.
  - 6ren 15y ago
    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.
    - gradstudent 15y ago
      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.
    - 15y ago

Bootvis 15y ago

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?

onemoreact 15y ago
Computer hardware is not correct. So, you need to step past mathematical perfection and write defensively. 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.
- nickik 15y ago
  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.
- exDM69 15y ago
  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.
  - onemoreact 15y ago
    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 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.
chokma 15y ago
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. http://www.sandroid.org/birdsproject/4dummies.html http://www.sandroid.org/birdsproject/4dummies.html gives a glimpse of how much fun developing software for aviation purposes is.
nickik 15y ago
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. You might injoy this darpa project: http://www.crash-safe.org/papers 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.

torstein 15y ago

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

jrockway 15y ago

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.)

bad_user 15y ago
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.
- arundelo 15y ago
  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.
  - nknight 15y ago

eternalban 15y ago

> 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.

DarkShikari 15y ago
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.
- nazgulnarsil 15y ago
  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?
  - wtallis 15y ago
    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.

6ren 15y ago

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>

adrianN 15y ago
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.
- 6ren 15y ago
  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.
  - gradstudent 15y ago
    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.
  - 15y ago