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: Georg Bauhaus <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: seL4 as base of an AdaOS with some Spark proofing?
Date: Thu, 31 Jul 2014 08:23:54 +0200
Organization: A noiseless patient Spider
Message-ID: <lrcndq$egl$1@dont-email.me>
References: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com>
 <NcaCv.85303$qR1.74779@fx02.iad> <lrc2of$36l$1@dont-email.me>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Thu, 31 Jul 2014 06:23:54 +0000 (UTC)
Injection-Info: mx05.eternal-september.org;
 posting-host="21136161de6819db887a6476fa794525";
	logging-data="14869"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+TcPusWr8RuGllM3DVPDHUhu9QR8XHiY8="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9;
 rv:24.0) Gecko/20100101 Thunderbird/24.6.0
In-Reply-To: <lrc2of$36l$1@dont-email.me>
Cancel-Lock: sha1:Q/qRApEXCeXn+zquPLnW343b9xI=
Xref: news.eternal-september.org comp.lang.ada:21366
Date: 2014-07-31T08:23:54+02:00
List-Id: <comp.lang.ada>

On 31/07/14 02:31, Simon Clubley wrote:
>> >(2) In-kernel ASM functions,
> It's not clear if they mean some assembly language kernel functions or
> if they are talking about the generated code from the compiler.
>

They explain that every kernel must have some assembly
language in it, and that theirs has some 300 lines of assembly.

Sounds like one can prove this amount of assembly code correct?