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-17 08:09:07 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!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: Sat, 17 Jan 2004 10:09:05 -0600 Date: Sat, 17 Jan 2004 11:09:04 -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-Z3dD9boQ9pZhCUhJIwjfR158fQvZ/tbU0NTvFwe3nrqy+EIKYWADWy56Z/DnfilB+BizUAEDjfL1hMA!oEvnhkecZa7z+F/gG3J6aHsBuc03hkYmyQ/KVa8woHinCSlHGl6gAi/IQ7pT/w== 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:4495 Date: 2004-01-17T11:09:04-05:00 List-Id: Aatu Koskensilta wrote: > So your original statement > > [any compiler for a resonable language] either does not accept some > legal programs, accepts some illegal programs, or never halts for some > inputs > > is correct if the reasonable language we're speaking about is Ada. I > think that, say, Haskell is a reasonable language, and the above does > not hold for it - the type system is decidable -, but perhaps you find > Haskell unreasonable. No, I used Ada as an example because everyone here should be familiar with it, and I am VERY familiar with where the bodies are buried, since I helped bury some of them. The proper way to describe my contention is probably: All realizable implementations of any programming language are finite. (This is because the hardware is a good, but finite, imitation of a Turing complete system.) If a language definition imposes limitations more restrictive than those imposed by the hardware, the programming language is finite. This is harder to do than it seems. For example, Java goes to extremes to insist that everything is a 32-bit quantity, including pointers. But it doesn't prevent say a 64-bit implementation from mapping larger physical addresses into 32-bit pointers. As a simple example, an implementation could insist that all addressable constructs begin on a 64-bit boundary and use 64-bit word addresses rather than 8-bit byte addresses. (Some Java implementations do use word addresses in pointers.) If the language is Turing complete, but the compiler runs on real hardware, then you can't use the compiler to tell the difference between physical limitations and cases where it is undecideable whether a program is illegal. You have to rely on analysis to recognize the later case. In particular, for Ada 83 I demonstrated a real case where the legality of a program was undecideable, and two compilers gave different (but correct) answers. Given time I can probably find similar cases for all Turing complete programming languages, including the usual suspects of Fortran, Cobol, C, and Ada 95. (C++ is so easy it seems like cheating.) But my real point is that compiler developers can't just wish away G�del's proof, and they don't. Good compilers are always careful to distinguish between cases where the compiler can decide that a program is illegal and cases where a submission exceeds the capabilities of the implementation, but may or may not be illegal. The example I gave was a rare case where a compiler could reach a conclusion about an undecideable case based on the run-time behavior of the code that compiler would generate. (And where two compilers were known to make different choices for the same hardware.) -- 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