From: Luke A. Guest <laguest@archeia.com>
Subject: Re: Kickstarter for beginning work on a new open-source Compiler
Date: Mon, 24 Mar 2014 06:16:56 +0000 (UTC)
Date: 2014-03-24T06:16:56+00:00 [thread overview]
Message-ID: <1137685828417334510.687294laguest-archeia.com@nntp.aioe.org> (raw)
In-Reply-To: OyPXu.74661$TT7.33733@fx23.iad
> (2) have the second be written in Ada 2012 (probably w/ SPARK
> verification/proving) -- hopefully w/ all annexes (though that's a LOT of
> work) -- and this would be the commercial product, then
> (3) have that compiler/PSE/IDE available for implementing a verified/proved OS.
>
> Like I said upthread; I believe that we /need/ our foundational tools to
> be without error... and that means investing in verification & correctness checking.
I had a quick look at spark 2012, and it stated that anything with pointers
can't be reliably verified. Good luck with that.
I think the spark stuff is really for embedded projects only.
Luke
next prev parent reply other threads:[~2014-03-24 6:16 UTC|newest]
Thread overview: 71+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-03-18 23:23 ANN: Kickstarter for beginning work on a new open-source Compiler Shark8
2014-03-19 9:06 ` Maciej Sobczak
2014-03-19 13:02 ` Peter Chapin
2014-03-19 13:48 ` Dmitry A. Kazakov
2014-03-19 22:11 ` Randy Brukardt
2014-03-20 14:56 ` Robert A Duff
2014-03-19 21:59 ` Randy Brukardt
2014-03-19 22:03 ` Randy Brukardt
2014-03-20 20:41 ` Shark8
2014-03-20 23:04 ` Randy Brukardt
2014-03-20 0:12 ` Luke A. Guest
2014-03-20 0:36 ` Peter Chapin
2014-03-20 0:52 ` Luke A. Guest
2014-03-20 12:10 ` Simon Wright
2014-03-20 12:45 ` Luke A. Guest
2014-03-20 13:22 ` Simon Wright
2014-03-20 14:13 ` Luke A. Guest
2014-03-20 14:17 ` J-P. Rosen
2014-03-21 2:13 ` Lucretia
2014-03-21 5:23 ` J-P. Rosen
2014-03-21 5:33 ` Lucretia
2014-03-21 6:43 ` J-P. Rosen
2014-03-21 22:51 ` Randy Brukardt
2014-03-22 1:13 ` Luke A. Guest
2014-03-22 6:27 ` Tero Koskinen
2014-03-22 7:02 ` J-P. Rosen
2014-03-24 20:50 ` Randy Brukardt
2014-03-24 22:42 ` Qun-Ying
2014-03-25 15:16 ` Tero Koskinen
2014-03-20 15:27 ` Robert A Duff
2014-03-20 21:06 ` Simon Wright
2014-03-21 16:07 ` Robert A Duff
2014-03-23 17:52 ` Simon Wright
2014-03-19 14:25 ` ANN: " Stephen Leake
2014-03-19 19:55 ` Shark8
2014-03-19 22:28 ` Randy Brukardt
2014-03-20 17:55 ` Shark8
2014-03-20 17:53 ` Dmitry A. Kazakov
2014-03-19 22:49 ` Brian Drummond
2014-03-20 10:21 ` Lucretia
2014-03-20 23:35 ` Stephen Leake
2014-03-21 8:17 ` Simon Wright
2014-03-23 21:14 ` erlo
2014-03-23 22:36 ` Simon Wright
2014-03-24 20:31 ` erlo
2014-03-19 21:04 ` Alan Browne
2014-03-19 22:22 ` Randy Brukardt
2014-03-20 20:30 ` Shark8
2014-03-21 2:18 ` Lucretia
2014-03-21 21:51 ` Shark8
2014-03-22 5:48 ` J-P. Rosen
2014-03-22 6:01 ` Jeffrey Carter
2014-03-24 21:03 ` Randy Brukardt
2014-03-22 9:14 ` Ludovic Brenta
2014-03-22 10:15 ` Pascal Obry
2014-03-22 10:25 ` Dirk Craeynest
2014-03-22 12:41 ` Niklas Holsti
2014-03-22 14:59 ` Dirk Craeynest
2014-03-22 16:20 ` Niklas Holsti
2014-03-22 17:05 ` Ludovic Brenta
2014-03-24 6:41 ` Shark8
2014-03-24 6:16 ` Luke A. Guest [this message]
2014-03-22 8:38 ` Dmitry A. Kazakov
2014-03-22 19:28 ` Stephen Leake
2014-03-22 20:39 ` Shark8
2014-03-24 1:16 ` Stephen Leake
2014-03-24 6:40 ` Shark8
2014-03-25 20:04 ` Stephen Leake
2014-03-25 20:30 ` Dmitry A. Kazakov
2014-03-20 21:35 ` gautier_niouzes
2014-03-21 22:19 ` Shark8
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox