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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII X-Google-Thread: 103376,a00006d3c4735d70 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2004-01-14 08:44:53 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!news-out.visi.com!petbe.visi.com!newsfeed.media.kyoto-u.ac.jp!newshosting.com!nx02.iad01.newshosting.com!216.196.98.140.MISMATCH!border1.nntp.ash.giganews.com!border2.nntp.sjc.giganews.com!border1.nntp.sjc.giganews.com!nntp.giganews.com!local1.nntp.sjc.giganews.com!nntp.comcast.com!news.comcast.com.POSTED!not-for-mail NNTP-Posting-Date: Wed, 14 Jan 2004 10:44:48 -0600 Date: Wed, 14 Jan 2004 11:44:47 -0500 From: "Robert I. Eachus" User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.4) Gecko/20030624 Netscape/7.1 (ax) X-Accept-Language: en-us, en MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Certified C compilers for safety-critical embedded systems References: <0F6Nb.1623$Tt.642@reader1.news.jippii.net> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit Message-ID: NNTP-Posting-Host: 24.34.214.193 X-Trace: sv3-3Q7PxHVGn92TINjFm2LCwq6SVck+cqfUzoOcin+CwxRmnzplsHvzFY6a0834krfw9aEJo9iK7UeCTyN!VZzzK4RjxK+5IM63p3Ss6/6CH+raGpeqlSoUo8Sr0GE0hlUwHreJDub7uDMTvQ== X-Complaints-To: abuse@comcast.net X-DMCA-Complaints-To: dmca@comcast.net X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.1 Xref: archiver1.google.com comp.lang.ada:4407 Date: 2004-01-14T11:44:47-05:00 List-Id: Georg Bauhaus wrote: > Can a self-hosting compiler then in theory decide whether it is > correct? For the former or the latter languages? I don't understand the question. Since this is posted in comp.lang.ada, it seems right to relate it to Ada compilers. There are two questions which seem similar, but are not. 1) Does this compiler correctly implement the Ada standard? We have validation tests, and any decent compiler development project extends those tests with a large library of regression tests, and runs them constantly as part of the ongoing support effort. In that sense Ada compilers are constantly testing to see whether they fail to implement the standard. Of course, not failing any existing test does not make the compiler perfect, it just means that there are no known bugs. 2) Can this compiler correctly compile all Ada programs? Of course not. Let me first quote from the Ada RM 1.1.3: "A conforming implementation shall: * Translate and correctly execute legal programs written in Ada, provided that they are not so large as to exceed the capacity of the implementation; * Identify all programs or program units that are so large as to exceed the capacity of the implementation (or raise an appropriate exception at run time); * Identify all programs or program units that contain errors whose detection is required by this International Standard; * Supply all language-defined library units required by this International Standard; * Contain no variations except those explicitly permitted by this International Standard, or those that are impossible or impractical to avoid given the implementation's execution environment; * Specify all such variations in the manner prescribed by this International Standard..." EVERY Ada compiler that currently exists has programs that are part of the validation suite that they fail to compile due to capacity limitations. Part of the validation process is to determine whether those limitations are in some sense "reasonable". So as far as G�del's proof is concerned, we know that all Ada compilers are incomplete implementations of Ada. We have accepted that incompleteness of Ada implementations as much to be preferred to compilers that accept illegal Ada programs, or worse, incorrectly recognize the meaning of a given Ada program. You may consider this a "dirty little secret" about programming languages and compilers if you want. I just consider it a fact of life. Also, keep in mind that most Ada compilers will accept very large G�del numbers, written in factored form or as constants with hundreds of digits. You can design a program so that it only accepts a program as legal Ada if a particular G�del number specifies a true theorem in G�del's formalization, and will reject it otherwise. As a practical matter, there will be large numbers of such programs where the compiler will eventually halt. In practice you won't want to wait that long. Of course, there are other theorems where either the compiler will reject the program due to implementation restrictions or the compiler will never halt, assuming a perfect machine to run the compiler on. It may be of great theoretical interest to know that a compilation that has already run for a day may not halt in a decade, or a century. But in practice the hardware (and probably the compiler) is just not that good. -- Robert I. Eachus "The war on terror is a different kind of war, waged capture by capture, cell by cell, and victory by victory. Our security is assured by our perseverance and by our sure belief in the success of liberty." -- George W. Bush