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=1.1 required=5.0 tests=BAYES_20,INVALID_DATE,
	MSGID_SHORT autolearn=no autolearn_force=no version=3.4.4
Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.2 9/18/84; site sftor.UUCP
Path: utzoo!watmath!clyde!burl!ulysses!mhuxr!mhuxn!mhuxm!sftig!sfmag!sftor!rajeev
From: rajeev@sftor.UUCP (S.Rajeev)
Newsgroups: net.lang.ada
Subject: Re: What I miss... (really C, Ada, religion)
Message-ID: <782@sftor.UUCP>
Date: Sat, 5-Oct-85 17:30:26 EDT
Article-I.D.: sftor.782
Posted: Sat Oct  5 17:30:26 1985
Date-Received: Sun, 6-Oct-85 07:14:07 EDT
References: <796@kuling.UUCP> <2580002@csd2.UUCP> <191@graffiti.UUCP> <568@unisoft.UUCP> <1777@orca.UUCP> <879@lll-crg.UUCP>
Organization: AT&T Bell Laboratories, Summit N.J.
List-Id: <comp.lang.ada>

> If you program has a proof of correctness,  ....

 That is a very big if. How many large programs do you know that have
even informal, let alone formal, proofs using verification methods?


-- 
{allegra,ihnp4}!attunix!rajeev   -- usenet
ihnp4!attunix!rajeev@BERKELEY   -- arpanet
Sri Rajeev, SF 1-342, Bell Labs, Summit, NJ 07901. (201)-522-6330.