Erik Naggum <clerik@naggum.no> wrote:
+---------------
| * Rob Warnock
| | 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! ...
|
| this argument, which is presented quite frequently, is hard to refute
| because it makes a number of assumptions that one needs to challenge at
| their root, not in their application.
+---------------
O.k., so I flippantly overstated the case. (But it *was* in a postscript to
an article [not quoted] in which I actually made the case *for* constructing
correct programs from their proofs, so I *do* have some respect for provability
concerns...]
+---------------
| another assumption is that specifications need to be as precise as the
| program is. this is not so.
+---------------
Not as "precise", but certainly as "correct", yes? You won't deny, I hope,
that incorrect specifications usually lead to incorrect functioning of the
total system, *especially* when the code is proven to implement the
specification!
+---------------
| specifications should contain what the code does not. in particular,
| preconditions and postconditions can be expressed (and checked) by other
| means than computing the value. invariants that are not expressed in
| code need to be provably maintained.
+---------------
The problem I was noting in that postscript was that in attempting to
prove *total system* correctness [as opposed to proving correctness of
an encapsulated library component, which is often fairly straightforward]
one eventually must regress (step back) to the initial human desires
that led to the specification -- whereupon one runs smack bad into
the "DWIS/DWIM" problem ("Don't do what I *said*, do what I *meant*!"),
which at its root contains the conundrum that much of the time we
humans don't actually *know* exactly what we want!
+---------------
| creating correct software is a lot easier than creating buggy software
| that works. however, if you start with buggy methodologies you'll never
| obtain correct software, and you might mistakenly believe that correct
| software is therefore impossible.
+---------------
We violently agree. However, I was trying to warn that that *still*
isn't enough to prevent disasters, since the best you'll ever get
with the best methodologies is code whose behavior meets the originally
stated goals... WHICH MAY HAVE BEEN WRONG.
Yet I think we also agree that the truth of this point is no excuse
for not using the best methodologies we have access to *anyway*...
-Rob
-----
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