From: ncohen@watson.ibm.com (Norman H. Cohen)
Subject: Re: Run-time checking and speed
Date: 13 Jan 1995 15:21:58 GMT
Date: 1995-01-13T15:21:58+00:00 [thread overview]
Message-ID: <3f65qm$jie@watnews1.watson.ibm.com> (raw)
In-Reply-To: 3f3deb$4us@gnat.cs.nyu.edu
In article <3f3deb$4us@gnat.cs.nyu.edu>, dewar@cs.nyu.edu (Robert Dewar)
writes:
|> Another situation where it is quite appropriate to turn off run time checks
|> is in verified safety critical code where part of the verification ensures
|> that the checks are not needed. You have to be *very* sure of your
|> verification technology to depend on this!
In the famous article "Social Processes and Proofs of Theorems and
Programs" (Communications of the ACM, May 1979), DeMillo, Lipton, and
Perlis wrote:
There is a tendency, as we begin to feel that a structure is
logically, provably right, to remove from it whatever redundancies
we originally built in because of lack of understanding. Taken to
its extreme, this tendency brings on the so-called Titanic effect;
when failure does occur, it is massive and uncontrolled. To put it
another way, the severity with which a system fails is directly
proportional to the intensity of the designer's belief that it cannot
fail. Programs designed to be clean and tidy merely so that they can
be verified will be particularly susceptible to the Titanic effect.
Already we see signs of this phenomenon. In their notes on Euclid, a
language designed for program verification, several of the foremost
verification adherents say, "Because we expect all Euclid programs to
be verified, we have not made special provisions for exception
handling.... Runtime software errors should not occur in verified
programs." Errors should not occur? Shades of the ship that
shouldn't be sunk.
The remark about "programs designed to be clean and tidy merely so that
they can be verified" is off base--such programs are more easily
understood by their writers and are therefore more reliable. However, we
should take seriously the warning about reliance on verification
technology (which has not advanced appreciably in the 16 years since the
article was written) in place of run-time checks.
(We should be equally wary, of course, of reliance on run-time checks in
place of reasoning about the correctness of a program. And given that
someone is going to remove checks anyway, a formal proof that it is safe
to do so is to be welcomed. At his summits with Gorbachev, Reagan was
fond of quoting the alleged Russian proverb, "Trust, but verify." When it
comes to ensuring the safety of a program, this would be better worded,
"Verify, but don't trust.")
--
Norman H. Cohen ncohen@watson.ibm.com
next prev parent reply other threads:[~1995-01-13 15:21 UTC|newest]
Thread overview: 18+ messages / expand[flat|nested] mbox.gz Atom feed top
1995-01-10 22:20 Run-time checking and speed Tony Leavitt
1995-01-12 1:14 ` Roger Labbe
1995-01-13 12:09 ` Philip Brashear
[not found] ` <3f0prq$3bq@theopolis.orl.mmc.com>
1995-01-12 14:13 ` Robert Dewar
1995-01-13 1:49 ` Doug Smith
1995-01-13 15:29 ` Norman H. Cohen
1995-01-13 15:21 ` Norman H. Cohen [this message]
[not found] ` <3fa2pk$kbi@felix.seas.gwu.edu>
[not found] ` <EACHUS.95Jan17151835@spectre.mitre.org>
[not found] ` <3fjhrj$9b3@oahu.cs.ucla.edu>
1995-01-20 5:11 ` Robert Dewar
1995-01-23 16:43 ` Mats Weber
1995-01-24 19:25 ` Robert Dewar
1995-01-22 18:43 ` Michael Feldman
1995-01-23 23:38 ` Robert Dewar
1995-01-26 16:14 ` Kent Mitchell
1995-01-28 6:03 ` Robert Dewar
[not found] ` <3gbr4f$p4b@theopolis.orl.mmc.com>
1995-01-29 13:00 ` Robert Dewar
1995-01-30 19:21 ` Garlington KE
1995-01-12 15:11 ` Norman H. Cohen
-- strict thread matches above, loose matches on Subject: below --
1995-01-12 15:54 Keith Arthurs
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox