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
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: seL4 as base of an AdaOS with some Spark proofing?
Date: Wed, 30 Jul 2014 13:55:31 +0200
Organization: A noiseless patient Spider
Message-ID: <lramfj$68f$1@dont-email.me>
References: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com>
 <lracht$8a9$1@dont-email.me> <drednZEea59sVkXO4p2dnAA@giganews.com>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 30 Jul 2014 11:55:32 +0000 (UTC)
Injection-Info: mx05.eternal-september.org;
 posting-host="b96887e80893c84a90c3007226ca0d1c";
	logging-data="6415"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/ySHh0XA+jO17FRfPxaGjkflrwXy6OnvU="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9;
 rv:24.0) Gecko/20100101 Thunderbird/24.6.0
In-Reply-To: <drednZEea59sVkXO4p2dnAA@giganews.com>
Cancel-Lock: sha1:ZMVRbZOjukefH/FC043mWt3zy+I=
Xref: news.eternal-september.org comp.lang.ada:21351
Date: 2014-07-30T13:55:31+02:00
List-Id: <comp.lang.ada>

On 30.07.14 12:41, Peter Chapin wrote:

> The question one must ask is: how difficult is it to do and how much
> "normal" code can you effectively prove?

Questions about the efficiency of coding/reasoning could well
be made economically interesting, I think. In this seL4
scenario, one is proving formal source text, and measuring
this effort could be done by using wall clock time (as usual),
that is: person hours, and processor time.

Looking at what they show, e.g., no buffer overflows, no
problems with arithmetic, avoiding certain pointer issues,
one could compare the difficulties of preventing these mostly
by construction, i.e., scalar types of Ada + GNATSpark, and
not by proving things after the fact.