From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=0.7 required=5.0 tests=BAYES_00,INVALID_DATE,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,9da298537a16487e
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 1995-01-13 07:21:58 PST
Path: 
 nntp.gmd.de!Germany.EU.net!howland.reston.ans.net!agate!darkstar.UCSC.EDU!news.hal.COM!olivea!uunet!newsgate.watson.ibm.com!watnews.watson.ibm.com!ncohen
From: ncohen@watson.ibm.com (Norman H. Cohen)
Newsgroups: comp.lang.ada
Subject: Re: Run-time checking and speed
Date: 13 Jan 1995 15:21:58 GMT
Organization: IBM T.J. Watson Research Center
Distribution: world
Message-ID: <3f65qm$jie@watnews1.watson.ibm.com>
References: <3ev16u$ojc@pong.lasc.lockheed.com>
 <3f0prq$3bq@theopolis.orl.mmc.com> <3f3deb$4us@gnat.cs.nyu.edu>
Reply-To: ncohen@watson.ibm.com
NNTP-Posting-Host: rios8.watson.ibm.com
Date: 1995-01-13T15:21:58+00:00
List-Id: <comp.lang.ada>

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