Brent A Ellingson <bellings@badlands.nodak.edu> wrote:
+---------------
| It is provably impossible to verify all code. This isn't myth -- this
| is fact...
+---------------
Yes, but...
+---------------
| ...software failures, *in general*, are NOT preventable.
+---------------
Yes, but... (Part of the problem is that "failure" isn't always a well-
defined technical term.)
+---------------
| Trying to verify code is good. Mistakenly believing it is possible
| to create "provably correct code" is like believing you can tell
| the future by a combination of voodoo and looking at the guts of a
| slaughtered goat. It can't be done. Period.
+---------------
True, but not a reason to throw up one's hands and "give up".
While it is true that one cannot in general prove an arbitrary already-
written program correct or incorrect (it's equivalent to "the halting
problem", which is provably not solvable in general), you can *construct*
correct programs by deriving them from their proofs. (Look in the literature
for what Dijkstra & Gries &c were doing a decade ago.)
Which leaves one a choice: If you want provably-correct programs, you *can*
start with a proof and derive the program from it. Or you can say, "It's
too hard to construct proofs of programs big enough to be interesting"
[despite some examples to the contrary], and blithely code away in whatever
style you fancy, but have no assurance that you'll ever be able to prove
anything (one way *or* the other) about your code ex post facto. (Though
*some* programs can be proved/disproved ex post facto, your program just
might be one of those uncountable number for which the program prover
never halts.) Your choice.
-Rob
p.s. Actually, to me the "provability" argument is somewhat silly.
Sure, I'd like all my code to be "correct", but IMHO the *real* problem
is that "correct" can only be defined in terms of a specification, and
one thing's for *damn* sure, there's no human way to create "provably
correct" specifications! (Or if you think there is, change "specifications"
to "requirements". Regress as necessary until you get back to human wants
and needs that led to the project [whatever it is] being instigated.
Let's see you "prove" something about *those*!)
-----
Rob Warnock, 7L-551 rpw3@sgi.com http://reality.sgi.com/rpw3/
Silicon Graphics, Inc. Phone: 650-933-1673 [New area code!]
2011 N. Shoreline Blvd. FAX: 650-933-4392
Mountain View, CA 94043 PP-ASEL-IA