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.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,f039470e8f537101
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-07-29 23:17:40 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!headwall.stanford.edu!newshub.sdsu.edu!elnk-nf2-pas!newsfeed.earthlink.net!stamper.news.pas.earthlink.net!stamper.news.atl.earthlink.net!harp.news.atl.earthlink.net!not-for-mail
From: Richard Riehle <richard@adaworks.com>
Newsgroups: comp.lang.ada
Subject: Re: Ariane5 FAQ
Date: Tue, 29 Jul 2003 23:19:54 -0700
Organization: AdaWorks Software Engineering
Message-ID: <3F27638A.888BAEC4@adaworks.com>
References: <mailman.26.1058753354.24167.comp.lang.ada@ada.eu.org>
 <wqkTa.18742$0F4.18264@nwrdny02.gnilink.net>
	 <pan.2003.07.23.00.31.01.14991@mail.utexas.edu>
	 <1058968422.225561@master.nyc.kbcfp.com> <3F200AD0.94F79098@adaworks.com>
	 <e2e5731a.0307241721.a6eae4e@posting.google.com>
	 <7u9Ua.13412$634.10307@nwrdny03.gnilink.net> <3F215120.1040706@attbi.com>
	 <1059151910.357790@master.nyc.kbcfp.com>
	 <e2e5731a.0307251844.7ea4dab4@posting.google.com>
	 <bDTUa.6456$AO6.976@nwrdny02.gnilink.net>
	 <e2e5731a.0307271419.4390a02c@posting.google.com> <ud6fvzbzc.fsf@xsol.com>
	 <3F248CEE.5050709@attbi.com> <3F25FB81.A81694FA@adaworks.com>
 <uispljeua.fsf@xsol.com>
Reply-To: richard@adaworks.com
NNTP-Posting-Host: 41.b2.48.58
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
X-Server-Date: 30 Jul 2003 06:17:39 GMT
X-Mailer: Mozilla 4.7 [en] (Win98; I)
X-Accept-Language: en
Xref: archiver1.google.com comp.lang.ada:40986
Date: 2003-07-30T06:17:39+00:00
List-Id: <comp.lang.ada>

Berend de Boer wrote:

> >>>>> "Richard" == Richard Riehle <richard@adaworks.com> writes:
>
>     Richard> systems than that found in Eiffel.  I am thinking here of
>     Richard> SPARK.
>
>     Richard> In general, the safety-critical community does not like
>     Richard> the Eiffel model because it relies on assertion-errors at
>     Richard> run-time.  While this is just fine for
>     Richard> non-safety-critical software, it is not appropriate for a
>     Richard> system such as Ariane V, or any other similar system.
>
> Nothing (perhaps some annoying mathematical proofs :-) ) precludes
> checking at compile time. I'm really hoping (probably have to write it
> myself it seems if I want to have it ))-: ) for SPARK for Eiffel. That
> would be a real step forward.

It would be a difficult step to take.  Eiffel includes some features that
are incompatible with the level of checking done by SPARK.   When
checking Ada code, SPARK is more conservative than Ada itself. I
suspect that SPARK would disallow some of the most interesting and
useful features of Eiffel.

Eiffel is, in its present form, an excellent language for a wide range
of applications.  I like it for anything not safety-critical.  It is
certainly
better  than C++ (sorry Hyman) in my opinion.   However, niether
C++ nor Eiffel quite meet the level one would require of safety-critical
software -- unless one emasculates the most interesting aspects of each
of those languages.   Although SPARK permits only a subset of Ada,
it leaves the essential features of Ada intact, even after its rigorous
checking.  This would not be true of C++ or Eiffel.

Richard Riehle