Subject: Re: dealing with errors (was: "Programming is FUN again")
From: (Rob Warnock)
Date: 1998/03/29
Newsgroups: comp.lang.lisp
Message-ID: <6fkjln$>

Erik Naggum  <> 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

|   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

|   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 Warnock, 7L-551
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