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: 103376,a00006d3c4735d70
X-Google-Attributes: gid103376,public
X-Google-Thread: f849b,b8d52151b7b306d2
X-Google-Attributes: gidf849b,public
X-Google-ArrivalTime: 2004-01-11 09:46:19 PST
Path: 
 archiver1.google.com!news1.google.com!sn-xit-02!sn-xit-01!sn-post-01!supernews.com!corp.supernews.com!not-for-mail
From: mojaveg@iwvisp.com (Everett M. Greene)
Newsgroups: comp.arch.embedded,comp.lang.ada
Subject: Re: Certified C compilers for safety-critical embedded systems
Date: Sun, 11 Jan 2004 09:44:14 PST
Organization: none that you'd notice
Message-ID: <20040111.79C2A20.8BC3@mojaveg.iwvisp.com>
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> <btqo11$8uo@libra
X-NewsReader: GRn 3.2n February 9, 1999
MIME-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: 8bit
X-Complaints-To: abuse@supernews.com
Xref: archiver1.google.com comp.arch.embedded:7273 comp.lang.ada:4337
Date: 2004-01-11T09:44:14-08:00
List-Id: <comp.lang.ada>

"John R. Strohm" <strohm@airmail.net> writes:
> "Hyman Rosen" <hyrosen@mail.com> wrote in message
> > 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.

It has been my observation that there's an inverse relation
between the difficulty in describing what's needed and the
difficulty in implementing it.  Perhaps this is just another
aspect of the specification difficulty -- once you've clearly
specified what's needed, it's not that difficult to implement
it.