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-10 19:26:29 PST
Path: 
 archiver1.google.com!news2.google.com!news.maxwell.syr.edu!newsfeed.media.kyoto-u.ac.jp!newsfeed.icl.net!newsfeed.fjserv.net!feed.news.tiscali.de!news.belwue.de!news.uni-stuttgart.de!news.rwth-aachen.de!not-for-mail
From: Hans-Bernhard Broeker <broeker@physik.rwth-aachen.de>
Newsgroups: comp.arch.embedded,comp.lang.ada
Subject: Re: Certified C compilers for safety-critical embedded systems
Followup-To: comp.arch.embedded
Date: 11 Jan 2004 03:26:29 GMT
Organization: Aachen University of Technology (RWTH)
Message-ID: <btqfp5$5ho$1@nets3.rz.RWTH-Aachen.DE>
References: <3fe00b82.90228601@News.CIS.DFN.DE>
   <11LvOkBBXw7$EAJw@phaedsys.demon.co.uk>
 <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>
    <AttdI2KzFEC2@eisner.encompasserve.org>
 <K5ydnZZB5rs1BWKi4p2dnA@comcast.com>
 <VK2Mb.2414$Qq.1124@nwrdny01.gnilink.net>
NNTP-Posting-Host: accip02.physik.rwth-aachen.de
X-Trace: nets3.rz.RWTH-Aachen.DE 1073791589 5688 137.226.33.41 (11 Jan 2004
 03:26:29 GMT)
X-Complaints-To: abuse@rwth-aachen.de
NNTP-Posting-Date: 11 Jan 2004 03:26:29 GMT
Xref: archiver1.google.com comp.arch.embedded:7246 comp.lang.ada:4323
Date: 2004-01-11T03:26:29+00:00
List-Id: <comp.lang.ada>

In comp.arch.embedded Hyman Rosen <hyrosen@mail.com> wrote:
> Robert I. Eachus wrote:
> > The Airbus 320 should bury the idea that theorem provers can result in 
> > safe software.

Well, saying they can't result in safe software would be even wronger,
of course.  So I guess the real idea that has to be buried is that
they _will_ do so, just like that.

Or, in other words: no matter how good your tools, the GIGO principle
(garbage in, garbage out) still holds.

> 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.

Which would appear to be one of many special cases of what we used to
call the "lemma on conservation of difficulty" among students here.
In the essence it says: "No truly difficult problems ever go away just
by waving some magical tool at them."

-- 
Hans-Bernhard Broeker (broeker@physik.rwth-aachen.de)
Even if all the snow were burnt, ashes would remain.