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=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,5412c98a3943e746 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Received: by 10.68.134.225 with SMTP id pn1mr2054093pbb.7.1331124143472; Wed, 07 Mar 2012 04:42:23 -0800 (PST) Path: h9ni49664pbe.0!nntp.google.com!news2.google.com!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail From: Stuart Newsgroups: comp.lang.ada Subject: Re: Verified compilers? Date: Wed, 7 Mar 2012 04:42:22 -0800 (PST) Organization: http://groups.google.com Message-ID: <15276255.3865.1331124143041.JavaMail.geo-discussion-forums@vbze11> References: NNTP-Posting-Host: 20.133.0.13 Mime-Version: 1.0 X-Trace: posting.google.com 1331124143 9490 127.0.0.1 (7 Mar 2012 12:42:23 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Wed, 7 Mar 2012 12:42:23 +0000 (UTC) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=20.133.0.13; posting-account=9gDAAwoAAACNb2IeoWuUI1mQDA83utl6 User-Agent: G2/1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Date: 2012-03-07T04:42:22-08:00 List-Id: On Tuesday, 6 March 2012 01:27:25 UTC, Randy Brukardt wrote: > "Yannick Duch=EAne (Hibou57)" <...> wrote in message=20 > news:op.v91cleyiule2fv@douda-yannick ... > >What do you think of this sentence, "now that he's found the right=20 > >architecture for building verified compilers, everyone will know how to = do=20 > >it?" >=20 > Why would anyone want to do it? This is *not* a problem area in compilers= =20 > (at least in my experience). When we introduced an intermediate code to= =20 > separate semantics from optimization from code generation, one of the=20 > unexpected benefits was that code generation bugs dropped to almost none. I admit I have not read the report yet - so I am unaware of the scope of th= e 'formal verification'; and Randy's post does point out other areas where = errors creep into the compilation process. That said, there is still an is= sue in safety-critical applications of constructing a robust and compelling= safety case, particularly covering the compilation process. This would se= em to be something that would aid in such cases. You note 'code generation bugs dropped to almost none' - but then say:- =20 > Bugs come from incorrectly converting semantics (which could not be=20 > "verified" unless a formal description of the source language exists, and= =20 > that has proven too hard to do for any real programming language - "a sub= set=20 > of C" not counting as such a language!). And most of all from optimizatio= ns;=20 > perhaps an optimizer could be formally verified but I suspect doing so wo= uld=20 > take 3 times as much work as fixing the bugs as they're found. The remark about optimization is interesting as [certainly up to a few year= s back] the number of target code generation faults seemed evenly balanced = between those that were caused during optimization and those that were fixe= d by optimization (i.e. the fault goes away when the compiler is allowed to= apply optimization strategies). Whichever stage of the compilation process is at fault, [in my experience] = there are usually a number of target code faults associated with fairly mat= ure compilers and these cases have to be managed by the safety case and dev= elopment processes. Getting people with the experience at both the high-level source and low-le= vel target code to review compilation issues is becoming increasingly diffi= cult. A technique that provides alternatives in verifying the compilation = process are attractive.