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: Wed, 30 Jul 2014 11:06:04 +0200
Organization: A noiseless patient Spider
Message-ID: <lracht$8a9$1@dont-email.me>
References: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 30 Jul 2014 09:06:05 +0000 (UTC)
Injection-Info: mx05.eternal-september.org;
 posting-host="b96887e80893c84a90c3007226ca0d1c";
	logging-data="8521"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19wseBUEiKLThaoeYXwR2zyK5c9B1nX+2Q="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9;
 rv:24.0) Gecko/20100101 Thunderbird/24.6.0
In-Reply-To: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com>
Cancel-Lock: sha1:3199NXCq9oT25/1kg0kD3KkS20U=
Xref: news.eternal-september.org comp.lang.ada:21349
Date: 2014-07-30T11:06:04+02:00
List-Id: <comp.lang.ada>

On 30/07/14 10:22, kug1977@web.de wrote:
> Doing an OS in Ada / Spark, might attract some people to use Ada instead of C.

Having an OS in Ada / GNATSpark available online might attract
some people to use Ada / GNATSpark instead of C.

Having an OS written in C that is proven correct and available
online shows that Ada / GNATSpark is not needed any more.

That's the impression, on first sight, that would need to be overcome IMHO.
You'd need three universities to switch proof setups, including languages,
for no apparent reason.