Nash wrote: >>
On Wed, Apr 13, 2005 at 11:01:11AM -0400, der Mouse wrote: > > Take the code for the checker. Wrap it in a small amount of code that > makes a deliberate out-of-bounds access if the checker outputs `no > problem'. Then write another small bit of code which ignores its > input and runs the wrapped checker on itself. > > Run the original checker on the result. > > This is basically the same diagonalization argument Turing used to > demonstrate that the Halting Problem was unsolvable; that's the sense > in which I call it the Halting Theorem rephrased. First off, I think you're more or less correct. Sortof. There is no computable predicate that will decide for any ARBITRARY PROGRAM whether ANY ARBITRARY CONSTRAINT is satisfied. But, this is just the statement of the fact that there are constraints that are, themselves, not computable. But, this is highly naive. A useful checker would not be designed to try to meet this objective. I think that's why he used the term "constrained environment." << Exactly. I'm not interested in trying to write a program prover that will prove that an arbitrary program is correct, if indeed it is. I am only interested in proving that well-structured programs are correct. This does of course constrain the software developer to write well-structured specifications and programs if she wants them to be proven correct; but I see such a constraint as a positive feature rather than a disadvantage, since it makes the resulting programs and specifications easier to understand. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com
