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=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable 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!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: Luke A. Guest Newsgroups: comp.lang.ada Subject: Re: Kickstarter for beginning work on a new open-source Compiler Date: Mon, 24 Mar 2014 06:16:56 +0000 (UTC) Organization: Aioe.org NNTP Server Message-ID: <1137685828417334510.687294laguest-archeia.com@nntp.aioe.org> References: <5151491a-14c3-4138-bcb5-f29108aeefb9@googlegroups.com> <9d599925-25ae-40c2-a26d-aa9fb7316649@googlegroups.com> <5B1Xu.64246$086.61049@fx18.iad> NNTP-Posting-Host: m5tTb2uN1MN59zrT4VbX/Q.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Complaints-To: abuse@aioe.org User-Agent: NewsTap/4.0.1 (iPhone/iPod Touch) X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:18941 Date: 2014-03-24T06:16:56+00:00 List-Id: > (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