>>> [B]uffer overflows can always be avoided, because if there is ANY >>> input whatsoever that can produce a buffer overflow, the proofs >>> will fail and the problem will be identified. >> Then either (a) there exist programs which never access >> out-of-bounds but which the checker incorrectly flags as doing so, >> or (b) there exist programs for which the checker never terminates >> (quite possibly both). (This is simply the Halting Theorem >> rephrased.) > Could you explain why you believe that proof of a specific property > in a constrained environment is equivalent to the Halting Problem?
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. > I really do find this line of argument rather irritating; the > theoretical limits of proof are quite a different thing from the > practical application of proof-based technology in a suitably > constrained environment. Entirely true. But if you use theoretical language like "proof", you have to expect to be held to a theroetical standard of correctness. /~\ The ASCII der Mouse \ / Ribbon Campaign X Against HTML [EMAIL PROTECTED] / \ Email! 7D C8 61 52 5D E7 2D 39 4E F1 31 3E E8 B3 27 4B
