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=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: State of the compiler market
Date: Sun, 26 Feb 2017 14:32:56 -0800
Organization: A noiseless patient Spider
Message-ID: <87mvd8k2g7.fsf@nightsong.com>
References: <a319aa93-f896-48ae-9b87-489b623ab75f@googlegroups.com>
	<1813789782.509760763.093426.laguest-archeia.com@nntp.aioe.org>
	<o8ted9$8lc$1@franka.jacob-sparre.dk> <87varxjouh.fsf@nightsong.com>
	<o8v3l1$3go$1@z-news.wcss.wroc.pl>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="ce4491607a11549426181c8f72c30fca";
	logging-data="31345"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+cFFUOaztGGGKCyybXiMDi"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:RJ7y9Fuj4zv27spnBmtqNAK6Gy0=
	sha1:SWx1c3kfYl70gac4DN0qpXSALhQ=
Xref: news.eternal-september.org comp.lang.ada:33422
Date: 2017-02-26T14:32:56-08:00
List-Id: <comp.lang.ada>

antispam@math.uni.wroc.pl writes:
>> team up with the CompCert guys and make a verified Ada compiler.
> Maybe a blasphemy here, but if you go trough full formal verification
> does Ada offer significant advantages over C or C++?

You mean if the application is verified?  Depends on what has been
verified, I suppose ;).  The idea of CompCert is just that the compiler
is verified so there's less worry about compiler bugs.  That's
independent of the verification processes you might use for your
application.

> L4.sec guys deliver code via C and apparently this did
> not hamper their efforts.

SEL4 is apparently around 10 KLOC of C and 480 KLOC of Isabelle/HOL
proofs, and the C was apparently produced (not sure whether manually or
automatically) by some kind of derivation from an executable
specficiation written in Haskell.  I haven't actually read the SEL4
papers but that comes from a quick glance.  They are accessible from
here:  http://ts.data61.csiro.au/projects/seL4/

> Ada strength is in intermediate area where better checking in compiler
> and safer programming practices lead to faster delivery of reasonably
> good program.

This is reasonable to say.  Also Ada's verification tools like SPARK
supply more automation than what's available for C as far as I can tell.