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-7-bit Received: by 10.68.220.229 with SMTP id pz5mr3687962pbc.5.1331168792265; Wed, 07 Mar 2012 17:06:32 -0800 (PST) MIME-Version: 1.0 Path: h9ni51652pbe.0!nntp.google.com!news2.google.com!npeer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nx02.iad01.newshosting.com!newshosting.com!news2.euro.net!news.mixmin.net!gandalf.srv.welterde.de!news.jacob-sparre.dk!munin.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Verified compilers? Date: Wed, 7 Mar 2012 19:06:28 -0600 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <15276255.3865.1331124143041.JavaMail.geo-discussion-forums@vbze11> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1331168791 12890 69.95.181.76 (8 Mar 2012 01:06:31 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 8 Mar 2012 01:06:31 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 X-Received-Bytes: 5218 Date: 2012-03-07T19:06:28-06:00 List-Id: "Stuart" wrote in message news:15276255.3865.1331124143041.JavaMail.geo-discussion-forums@vbze11... On Tuesday, 6 March 2012 01:27:25 UTC, Randy Brukardt wrote: ... > I admit I have not read the report yet - so I am unaware of the scope of > the 'formal verification'; > and Randy's post does point out other areas where errors creep into the > compilation process. > That said, there is still an issue in safety-critical applications of > constructing a robust and > compelling safety case, particularly covering the compilation process. > This would seem to be > something that would aid in such cases. I thought about that some after posting my reply. I probably was a bit too flippant. The real problem is that the only languages that can practically be verified are extremely simple, and I suspect it usually would be a bad idea to code large systems in such languages. (All of the advantages of a language like Ada -- or even C++ -- would be thrown away. After all, that's my complaint about SPARK, and this would be many times worse.) ... > Whichever stage of the compilation process is at fault, [in my experience] > there are usually > a number of target code faults associated with fairly mature compilers and > these cases have > to be managed by the safety case and development processes. True enough. But I don't think that it would be all that practical to verify an entire compiler for a real programming language. Moreover, I doubt that it would take any special architecture to do so, just a reasonable partitioning of concerns. It surely would be "easy" to verify the translation of our intermediate code to machine code (particularly if small simplifications were made in both; a formal definition would be needed for the intermediate code, but that would not be hard to do - it's already defined by Ada source code and carefully documented in English). It probably would be practical to verify the intermediate code transformations of an optimizer (not ours, however). Verifying the translation of raw syntax to intermediate code would be harder, and would mainly depend on a formal definition of the source language (which as noted, would be impossible to provide for any real language; part of the problem being that no human could understand it well enough to know if it is right -- so would verifying that it is translated properly really provide any benefit??). > Getting people with the experience at both the high-level source and > low-level target code > to review compilation issues is becoming increasingly difficult. A > technique that provides > alternatives in verifying the compilation process are attractive. Understood, but as noted I'm dubious that this would really help. You could verify *some* language, but whether it really was the same language that you wanted would be impossible to tell. I suppose if you could hook up a SPARK-like verifier to it, you could see if your program did what you want based on the formal description -- whether that actually matched the expected semantics or not -- but that would require describing the intended outputs of your program in the language of the formal description, and I'm dubious that you could understand *that* well enough to tell if it really did what you want. And if you succeeded in doing that, you no longer need the program itself -- it's just an artifact, you might as well directly translate the formal specification into code -- at which point you have to start the entire cycle again. (Can you tell that I think trying to verify everything is a waste of time, not matter what it is??) Anyway, it's certainly true that some programming problems need extraordinary measures. And I suppose for those people, this sort of thing will appear to be a new silver bullet. But of course there is no silver bullet for programming - it's hard, it is going to remain hard, and worrying too much about the compiler when the source program is hardly verified at all makes little sense. Randy.