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-21 15:23:18 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!c03.atl99!sjc70.webusenet.com!news.webusenet.com!pd7cy2so!shaw.ca!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, 21 Jan 2004 17:23:13 -0600 Date: Wed, 21 Jan 2004 18:23:12 -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: 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-oCl2cBenjYaEMWhxYM6X/oqRMkS5zfmXO84HGSEdBUgGQijrbEsIEwLme7+MOFOlx3zvVUYW3PLgKcU!syosmzIxETwCK1haAvEa3F+QFY3uTHQxfK1qW7rFUNDryFp9ITDtNoHX3q0QaQ== 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:4622 Date: 2004-01-21T18:23:12-05:00 List-Id: Aatu Koskensilta wrote: >> The Halting problem and G�del's proof are two sides of the same coin, >> at least in computer science. The Halting problem is a constructive >> proof of G�del's proof. > > > How is that? In what sense was G�del's original proof non-constructive? I didn't say that. What I meant (and think I said) was that in Computer Science showing that a computer language allows you to write the proof by contradiction in the Halting problem is the easiest way to prove by example that, for a given language, undecidability applies at a fundamental level. > Why is this relevant to the question of whether a compiler can correctly > recognise all legal programs and reject all illegal ones? Most languages > do not define "legal" by means of undecidable run-time behaviour. But most languages do define what programs are legal in an implementation independent manner. As I said here before, there are languages which can be recognized by a finite state machine. For such languages, it is clear that recognition is a decidable problem. The next step up is to languages which can require an arbitrary/indefinite (your choice of word) amount of retained state do determine whether or not a program is legal. Once you show that for any amount state, there is a program that requires more retained state to determine whether it is legal, you are done. > Perhaps Ada is different here. You mentioned earlier that producing a > C++ program which would defeat a given compiler was "trivial". Could you > provide some details? The easiest for most C++ programs is to create two program identifiers that hash/mangle to the same value. The "Birthday Paradox" usually makes a computer search for such a pair not too hard, even if the mangled names are large enough--and the mangling algorithm is complex enough--to make it hard to find a name that mangles to match a single existing name. A good C++ implementation could prefent the resulting program from compiling and linking, but it can't produce a working executable. And of course, a program that has one of the two names as a linkname is perfectly fine. -- 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