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!feeder.eternal-september.org!news.unit0.net!news.nask.pl!news.nask.org.pl!newsfeed.pionier.net.pl!pwr.wroc.pl!news.wcss.wroc.pl!not-for-mail From: antispam@math.uni.wroc.pl Newsgroups: comp.lang.ada Subject: Re: State of the compiler market Date: Mon, 27 Feb 2017 03:54:02 +0000 (UTC) Organization: Politechnika Wroclawska Message-ID: References: <1813789782.509760763.093426.laguest-archeia.com@nntp.aioe.org> <87varxjouh.fsf@nightsong.com> <87mvd8k2g7.fsf@nightsong.com> <877f4cjqcn.fsf@nightsong.com> NNTP-Posting-Host: hera.math.uni.wroc.pl X-Trace: z-news.wcss.wroc.pl 1488167642 23842 156.17.86.1 (27 Feb 2017 03:54:02 GMT) X-Complaints-To: abuse@news.pwr.wroc.pl NNTP-Posting-Date: Mon, 27 Feb 2017 03:54:02 +0000 (UTC) Cancel-Lock: sha1:jKQekv32kiQtoGEB1EprSSwJ5jA= User-Agent: tin/2.2.1-20140504 ("Tober an Righ") (UNIX) (Linux/4.9.5 (x86_64)) Xref: news.eternal-september.org comp.lang.ada:33426 Date: 2017-02-27T03:54:02+00:00 List-Id: Paul Rubin wrote: > antispam@math.uni.wroc.pl writes: > > Once you have verified compilation process it is natural to go for > > full formal verfication, from specification to machine code. > > Of course that's a very complicated process that's not always feasible. > > >> SEL4 is apparently around 10 KLOC of C and 480 KLOC of .. proofs > > > according to their time report writing C code took less > > than 15% of total time > > Given that it was 2% of the code per the above, 15% of the time doesn't > make it sound easy. That 15% included related proof annotations -- going from verified Haskell to verified C. > > Few years ago I talked with guy from Microsoft Research doing formal > > verfication. He claimed that their tools checked more things than > > SPARK. > > I can believe that, especially with older versions of SPARK. I'd be > interested to know which verification system the guy was describing. He was from M. Leino group. IIRC system in question were boogie and VCC. > > Main point was availability of quite strong proof engine and automatic > > generation of intermediate conditions. > > Stuff is certainly getting better. -- Waldek Hebisch