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 18:54:16 -0800
Organization: A noiseless patient Spider
Message-ID: <877f4cjqcn.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> <87mvd8k2g7.fsf@nightsong.com>
	<o903fo$l3j$1@z-news.wcss.wroc.pl>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="7a6fa5b8a21c48ff09386be160016fd3";
	logging-data="15861"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1936DKaNgvKOd5M8FOQjpI+"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:giN1mQGcMHhSt9d4L7j9VIYjuQM=
	sha1:LB59FAczU+QfmsHdRRuIkDs4hpw=
Xref: news.eternal-september.org comp.lang.ada:33425
Date: 2017-02-26T18:54:16-08:00
List-Id: <comp.lang.ada>

antispam@math.uni.wroc.pl writes:
> Once you have verified compilation process it is natural to go for
> full formal verfication, from specification to machine code.

Of course that's a very complicated process that's not always feasible.

>> SEL4 is apparently around 10 KLOC of C and 480 KLOC of .. proofs

> according to their time report writing C code took less
> than 15% of total time

Given that it was 2% of the code per the above, 15% of the time doesn't
make it sound easy.

> Few years ago I talked with guy from Microsoft Research doing formal
> verfication.  He claimed that their tools checked more things than
> SPARK. 

I can believe that, especially with older versions of SPARK.  I'd be
interested to know which verification system the guy was describing.

> Main point was availability of quite strong proof engine and automatic
> generation of intermediate conditions.

Stuff is certainly getting better.