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.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,4f9979b0d8705f9
X-Google-Attributes: gid103376,public
From: Peter Amey <pna@praxis-cs.co.uk>
Subject: Re: an you get this for me?
Date: 1998/06/11
Message-ID: <358057FA.1033@praxis-cs.co.uk>#1/1
X-Deja-AN: 361717978
Content-Transfer-Encoding: 7bit
References: <357FE61F.B8F81BFC@boeing.com>
Content-Type: text/plain; charset=us-ascii
Organization: Praxis Critical Systems
Mime-Version: 1.0
Newsgroups: comp.lang.ada,Michelle,Swift,<michelle.swift@pss.boeing.com>
Date: 1998-06-11T00:00:00+00:00
List-Id: <comp.lang.ada>


> 
> 4. Safer C by Les Hatton discusses use of C in safety critical systems
> and contains a comparision with Ada.
> 

I recommend treating this book with a certain amount of caution;  it manages 
to draw some rather bizarre conclusions.

For example, Les Hatton points to the existence of SPARK as some sort of 
proof that Ada must be "dangerous" - why invent a secure subset if the 
language is already "safe"?  The reality, of course, is that it is only 
_because_ the basic foundations of Ada are so good that is was possible to 
define SPARK.  A useable subset of C with SPARK's properties would be very 
difficult to produce (and it certainly wouldn't be a high-level language 
with support for abstraction etc.).  A SPARK-like subset of C++ is probably 
impossible.

Having dismissed Ada he then goes on to show that C is ok (providing you 
don't make any mistakes) and you use rafts of (his) tools to bring checking 
up to about the level of that performed by an Ada compiler.

George Romanski of Aonix has quite a good review of the book which I think 
is available from their web site.

Safety-critical systems involve unique problems including the need to be 
able to demonstrate, prior to any in-service experience, that the system 
_will_ be safe when deployed.  An essential basis for such a demonstration 
is a programming language with clear semantics that can be reasoned about.  
Ada is probably the only commercially-supported foundation on which such a 
language can built.

-- 
--------------------------------------------------------------------------- 
  
      __         Peter Amey, Product Manager
        )                    Praxis Critical Systems Ltd
       /                     20, Manvers Street, Bath, BA1 1PX
      / 0        Tel: +44 (0)1225 466991
     (_/         Fax: +44 (0)1225 469006
                 http://www.praxis-cs.co.uk/
 --------------------------------------------------------------------------