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=-2.9 required=5.0 tests=BAYES_00,MAILING_LIST_MULTI autolearn=unavailable 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 17:30:29 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!newsfeed.icl.net!newsfeed.fjserv.net!oleane.net!oleane!freenix!enst.fr!melchior!cuivre.fr.eu.org!melchior.frmug.org!not-for-mail From: "Alexandre E. Kopilovitch" Newsgroups: comp.lang.ada Subject: Re: Certified C compilers for safety-critical embedded systems Date: Thu, 15 Jan 2004 04:28:59 +0300 (MSK) Organization: Cuivre, Argent, Or Message-ID: References: NNTP-Posting-Host: lovelace.ada-france.org Mime-Version: 1.0 Content-Type: text/plain; charset=koi8-r Content-Transfer-Encoding: 8bit X-Trace: melchior.cuivre.fr.eu.org 1074130110 5720 80.67.180.195 (15 Jan 2004 01:28:30 GMT) X-Complaints-To: usenet@melchior.cuivre.fr.eu.org NNTP-Posting-Date: Thu, 15 Jan 2004 01:28:30 +0000 (UTC) To: comp.lang.ada@ada-france.org Return-Path: In-Reply-To: ; from Aatu Koskensilta at Wed, 14 Jan 2004 18:32:46 +0200 X-Mailer: Mail/@ [v2.44 MSDOS] X-Virus-Scanned: by amavisd-new-20030616-p5 (Debian) at ada-france.org X-BeenThere: comp.lang.ada@ada-france.org X-Mailman-Version: 2.1.3 Precedence: list List-Id: Gateway to the comp.lang.ada Usenet newsgroup List-Unsubscribe: , List-Post: List-Help: List-Subscribe: , X-Original-Content-Transfer-Encoding: 8bit Xref: archiver1.google.com comp.lang.ada:4418 Date: 2004-01-15T04:28:59+03:00 Aatu Koskensilta wrote: > >> [any compiler for a resonable language] either does not accept some > >> legal programs, accepts some illegal programs, or never halts for some > >> inputs > >> > >>does not in any sense > > > > Hm, _any_? How can you know about _any_ sense? There may be a sense of which > > you just aren't aware (for example, a sense of _real_ general-purpose > > programming languages and _real_ requirements for _really_used_ compilers > > for those languages -;). > > Then the impossibility follows from some constraints imposed by these > "reality" requirements, whatever they are, and not from G�del's theorem G�del's theorem here is not a foundation or cause, but an explanation of a fact from reality, which was observed many times. This theorem (like any other logical or mathematical theorem) does not exist in reality, so no one actually observable fact can _follow_ from that theorem in logical or mathematical sense. But the theorem is an idealized construct, a clean model, which may or may not be sufficiently adequate to some real situation. And that is what I'd like to say: if you don't know enough about _both_ sides of a correspondence, you can't reasonably judge about its adequacy. It does not matter how deep is your knowledge about one side of the correspondence, if you know too little about another side of it - in this case, have too little experience with internals of production-line compilers, and its real usage in sufficient scale. > >>follow from G�del's proof. > > > > > > It can't formally follow - just because the quoted statement is not formal - > > it couples the formal part with informal part, and the latter refers to a hard > > reality. So, the statement isn't a logical conclusion, it is an opinion about > > relationship between a particular logical construct and a piece of reality. > > It isn't. There's a very clear sense in which the above claim can be > taken to be about recursive functions - in which case all sorts of > considerations about hard relaity are obviously irrelevant -, in this > case about recursive functions that perform transformations on strings. Well, people are different, and some things that happen to be very clear for you, sound like absolute nonsense for me - I simply can't get (and don't want to) why those recursive functions appeared here - they seem (for me, of course) much more irrelevant here than my references to reality. > In hard reality there are very few correct compilers if any, but this > has nothing to do with G�del's theorem or its proof. Perhaps you consider G�del's theorem as a property of logicians, which is licensed (with some strict conditions) to computer scientists... If so, I must disappoint you - not all people agree with that position -:) Alexander Kopilovitch aek@vib.usr.pu.ru Saint-Petersburg Russia