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.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: f849b,b8d52151b7b306d2
X-Google-Attributes: gidf849b,public
X-Google-Thread: 103376,a00006d3c4735d70
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2004-01-10 21:49:12 PST
Path: 
 archiver1.google.com!news2.google.com!news.maxwell.syr.edu!c03.atl99!news.webusenet.com!newscene!novia!novia!news.airnews.net!cabal12.airnews.net!usenet
From: "John R. Strohm" <strohm@airmail.net>
Newsgroups: comp.arch.embedded,comp.lang.ada
Subject: Re: Certified C compilers for safety-critical embedded systems
Date: Sat, 10 Jan 2004 23:43:46 -0600
Organization: Airnews.net! at Internet America
Message-ID: <btqo11$8uo@library1.airnews.net>
References: <3fe00b82.90228601@News.CIS.DFN.DE>
 <3ff0687f.528387944@News.CIS.DFN.DE> <1086072.fFeiH4ICbz@linux1.krischik.com>
 <3ff18d4d.603356952@News.CIS.DFN.DE> <1731094.1f7Irsyk1h@linux1.krischik.com>
 <3ff1b8ef.614528516@News.CIS.DFN.DE> <3FF1E06D.A351CCB4@yahoo.com>
 <3ff20cc8.635997032@News.CIS.DFN.DE> <bsumbs$k9e$2@a1-hrz.uni-duisburg.de>
 Organization: LJK Software <AttdI2KzFEC2@eisner.encompasserve.org>
 <K5ydnZZB5rs1BWKi4p2dnA@comcast.com>
 <VK2Mb.2414$Qq.1124@nwrdny01.gnilink.net>
X-A-Notice: References line has been trimmed due to 512 byte limitation
Abuse-Reports-To: abuse at airmail.net to report improper postings
NNTP-Proxy-Relay: library1-aux.airnews.net
NNTP-Posting-Time: Sat, 10 Jan 2004 23:47:13 -0600 (CST)
NNTP-Posting-Host: ![H>C1k-WIj/(+q (Encoded at Airnews!)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2800.1106
X-MIMEOLE: Produced By Microsoft MimeOLE V6.00.2800.1106
Xref: archiver1.google.com comp.arch.embedded:7250 comp.lang.ada:4324
Date: 2004-01-10T23:43:46-06:00
List-Id: <comp.lang.ada>

"Hyman Rosen" <hyrosen@mail.com> wrote in message
news:VK2Mb.2414$Qq.1124@nwrdny01.gnilink.net...
> Robert I. Eachus wrote:
> > The Airbus 320 should bury the idea that theorem provers can result in
> > safe software.
>
> It's always been my contention that writing the specifications which you
> will then prove that a program obeys is exactly as hard as writing the
> program itself.

Yes and no.

Yes, in that writing rigorous formal specifications is HARD WORK.

No, in that the effort you put into writing those rigorous formal specifications
almost always translates into significantly-reduced effort when writing the code
that implements those specifications, because now you have a SOLID
understanding, where you used to have only a sketchy understanding.