From ...
From: Erik Naggum <clerik@naggum.no>
Subject: Re: dealing with errors (was: "Programming is FUN again")
Date: 1998/03/28
Message-ID: <3100091181606046@naggum.no>#1/1
X-Deja-AN: 338599620
References: <bc-1003981239050001@17.127.10.22> <351A72C3.5CEF1977@badlands.nodak.edu> <3099927027198005@naggum.no> <351BC8A3.7CE38A98@badlands.nodak.edu> <6fihvl$7bdrd@fido.asd.sgi.com>
mail-copies-to: never
Organization: Naggum Software; +47 8800 8879; http://www.naggum.no
Newsgroups: comp.lang.lisp


* 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!  (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*!)

  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.  I'll try, in no particular order.

  one assumption is that _all_ code should be provably correct, and that in
  the face of very hard cases one can somehow deduce something about the
  general provability issues.  this is not so.  an important argument in
  verifiable programming is that that which is encapsulated should be
  verified so you can trust your abstractions.  without this requirement,
  there is no upper bound to the complexity of proving anything, and those
  who argue against verification (or its costs) frequently assume that they
  will always deal with unverified code.  this is obviously not the case --
  people who have worked with these things for years have most probably
  done something pretty smart to make their work bear fruit, and so the
  often quite silly arguments about the fruitlessness of their endeavor are
  only true if you never verify anything.  this is somewhat like asking
  "but how would the stock market work if the government set all prices?"

  another assumption is that specifications need to be as precise as the
  program is.  this is not so.  code contains a lot of redundancy of
  expression and information and little expression of intent and purpose.
  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.  given such intents of the system
  that never get expressed in code, a specification can be fairly simple,
  and inconsistencies in a specification are far easier to spot than in a
  program.

  yet another assumption is that code would be allowed to be written with
  the same messy interaction of abstraction levels that programmers tend to
  use today.  this is not going to be allowed.  to make verification work,
  more information must be made explicit, while in most languages amenable
  to verification, the redundancy in information is minimized.  this latter
  point is also worth underlining: not just any language can be subject to
  verification.  C and C++, for instance, have so complex semantics that it
  is very hard to figure out what is actually going on unless the code is
  exceptionally cleanly written.

  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.

#:Erik
-- 
  religious cult update in light of new scientific discoveries:
  "when we cannot go to the comet, the comet must come to us."