jlg@lanl.gov (Jim Giles) (01/05/91)
From article <2474@motcsd.csd.mot.com>, by lance@motcsd.csd.mot.com (lance.norskog): > [...] > A program doesn't "work" because you (or somebody) thinks it works. > A program "works" if it can be mathematically proven to work. Experience > and operational time don't count. This isn't like quantum physics where > observation decides the matter. Empirical evidence doesn't enter into it. I must (at least partly) disagree with this. A correctness proof is of similar complexity to the program it "proves" and is just as prone to errors as the program is. (This possibility of error is present in _all_ mathematical proofs - which is why mathematics requires peer review and double-checking by other mathematicians. No programmer I know of submits his correctness proofs to such scrutiny.) To be sure, correctness proofs identify _some_ bugs in the program and are valuable as debugging tools. But such proofs aren't _replacements_ for all the other debugging tools. I think your mistake here is picking on the word "work". A program works if it performs acceptably _most_ of the time. If the cost of fixing the last few bugs in a program is greater than the cost of living with those bugs in place - don't bother fixing them. In a practical world, _only_ empirical evidence matters. By your definition of "work", _none_ of the UNIX environment does so. Come to think of it, maybe you're right after all :-). J. Giles
brnstnd@kramden.acf.nyu.edu (Dan Bernstein) (01/05/91)
In article <10370@lanl.gov> jlg@lanl.gov (Jim Giles) writes: > which is why mathematics requires peer > review and double-checking by other mathematicians. No programmer > I know of submits his correctness proofs to such scrutiny. Well, one programmer not only published his correctness proofs as models, but constructed his programs to be provable from the start. He had so much faith in his correctness proofs that he didn't even test the programs. As we all know, some of the code was buggy. A flaw in a theorem brings the whole deck of cards tumbling down because the *only* important thing in mathematics is truth. In contrast, as you pointed out, a bug in a program generally doesn't render the program useless. So it makes sense that the criteria for success in the two disciplines should be different. ) To be sure, > correctness proofs identify _some_ bugs in the program and are valuable > as debugging tools. But such proofs aren't _replacements_ for all the > other debugging tools. Quite right. ---Dan
rick@tetrauk.UUCP (Rick Jones) (01/07/91)
In article <10370@lanl.gov> jlg@lanl.gov (Jim Giles) writes: >From article <2474@motcsd.csd.mot.com>, by lance@motcsd.csd.mot.com (lance.norskog): >> [...] >> A program doesn't "work" because you (or somebody) thinks it works. >> A program "works" if it can be mathematically proven to work. Experience >> and operational time don't count. This isn't like quantum physics where >> observation decides the matter. Empirical evidence doesn't enter into it. > >I must (at least partly) disagree with this. A correctness proof is >of similar complexity to the program it "proves" and is just as prone >to errors as the program is. (This possibility of error is present in >_all_ mathematical proofs - which is why mathematics requires peer >review and double-checking by other mathematicians. No programmer >I know of submits his correctness proofs to such scrutiny.) To be sure, >correctness proofs identify _some_ bugs in the program and are valuable >as debugging tools. But such proofs aren't _replacements_ for all the >other debugging tools. They also only get you part of the way. Suppose you have proved your program correct, this can only be in terms of the language(s) in which it is written and possibly specified. This still doesn't prove that it will work in practice unless you have also proven correct the compiler, assembler, linker (and whatever other levels of translation are involved), as well as the CPU design, microcode (if a CISC machine), and indeed the entire hardware environment. (How many programs do you know that have work-rounds in them because code that _should_ work according to the language definition in fact doesn't?) This is almost like trying to prove mathematically that the universe works. In this case the boot is on the other foot; the universe works by definition, it is the job of mathematics and theoretical physics to find the methods to describe mathematically what is known empirically to be true. If my program "works", the fact that I can't prove it is a failure of the proving methods, not a failure of the program. -- Rick Jones Tetra Ltd. Maidenhead, Was it something important? Maybe not Berks, UK What was it you wanted? Tell me again I forgot rick@tetrauk.uucp -- Bob Dylan
ian@oravax.UUCP (Ian Sutherland) (01/10/91)
In article <1070@tetrauk.UUCP> rick@tetrauk.UUCP (Rick Jones) writes: >In article <10370@lanl.gov> jlg@lanl.gov (Jim Giles) writes: >>From article <2474@motcsd.csd.mot.com>, by lance@motcsd.csd.mot.com (lance.norskog): >>I must (at least partly) disagree with this. A correctness proof is >>of similar complexity to the program it "proves" Not always. Sometimes, especially in the case of proofs that are constructed in a mechanical theorem proving environment, the proof's complexity is much greater! If reasonable use is made of decisions procedures, it can be less. >>and is just as prone >>to errors as the program is. This is not so relevant if you don't see program proofs as iron-clad guarantees that the program will never disappoint you with what it does. If a proof, correct or incorrect, points out an error, then it's been of use. >>To be sure, >>correctness proofs identify _some_ bugs in the program and are valuable >>as debugging tools. But such proofs aren't _replacements_ for all the >>other debugging tools. Amen. >They also only get you part of the way. Suppose you have proved your program >correct, this can only be in terms of the language(s) in which it is written >and possibly specified. This still doesn't prove that it will work in practice >unless you have also proven correct the compiler, assembler, linker (and >whatever other levels of translation are involved), as well as the CPU design, >microcode (if a CISC machine), and indeed the entire hardware environment. I don't have statistics at my finger tips for this, but I believe the vast majority of programming errors occur at the source code level, and are not due to errors in compilers, hardware, etc. >If my program "works", the fact that I can't prove it is a failure of the >proving methods, not a failure of the program. Many a program has seemed to "work" for a very long stretch of time before bugs were discovered. Some of these bugs would have been found by proof. -- Ian Sutherland ian@oracorp.com Sans peur