This is a bit off-topic, but hopefully interesting. Rather than trying to prove a program to be correct (which I agree is doomed to failure for the forseeable future for all but trivial programs), perhaps it would be useful to have an automated therom-prover to try to deduce "interesting things" about certain programs such as "this program always bounds-checks its input", "this program allows writes to arbitrary files on lines x, y, and z", "this program halts". (:>) Obviously (as the last example illustrates), this isn't perfect because something can be true without being provable. Further, it's likely that assumptions must be made about system calls, libraries, and the ways in which they interact. There's also the problem of "who proves the prover". However, I think such a tool would be useful because it may quickly point out things not obvious to (most) humans and getting some idea of what can't be deduced and why would be instructive. | (Douglas) Hofstadter's Law: Frank Stuart | It always takes longer than you expect, even fstuart@vetmed.auburn.edu | when you take into account Hofstadter's Law.