From: Georg Bauhaus <bauhaus@futureapps.invalid>
Subject: Re: seL4 as base of an AdaOS with some Spark proofing?
Date: Wed, 30 Jul 2014 11:06:04 +0200
Date: 2014-07-30T11:06:04+02:00 [thread overview]
Message-ID: <lracht$8a9$1@dont-email.me> (raw)
In-Reply-To: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com>
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.
next prev parent reply other threads:[~2014-07-30 9:06 UTC|newest]
Thread overview: 16+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-07-30 8:22 seL4 as base of an AdaOS with some Spark proofing? kug1977
2014-07-30 9:06 ` Georg Bauhaus [this message]
2014-07-30 10:41 ` Peter Chapin
2014-07-30 11:55 ` G.B.
2014-07-30 17:47 ` Shark8
2014-07-30 22:40 ` Peter Chapin
2014-07-30 22:53 ` Shark8
2014-07-31 0:31 ` Simon Clubley
2014-07-31 6:23 ` Georg Bauhaus
2014-07-30 17:58 ` anon
2014-07-31 22:03 ` gvdschoot
2014-08-01 7:42 ` kug1977
2014-08-01 8:27 ` gvdschoot
2014-08-01 9:04 ` gvdschoot
2014-08-01 19:32 ` Randy Brukardt
2014-08-01 19:17 ` anon
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox