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-13 14:20:39 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!newsfeed.stueberl.de!teaser.fr!usenet-fr.net!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: Wed, 14 Jan 2004 01:18:48 +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 1074032310 93301 80.67.180.195 (13 Jan 2004 22:18:30 GMT) X-Complaints-To: usenet@melchior.cuivre.fr.eu.org NNTP-Posting-Date: Tue, 13 Jan 2004 22:18:30 +0000 (UTC) To: comp.lang.ada@ada-france.org Return-Path: In-Reply-To: ; from Aatu Koskensilta at Tue, 13 Jan 2004 15:28:43 +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:4375 Date: 2004-01-14T01:18:48+03:00 Aatu Koskensilta wrote: > > Anyone who works on compiler front end and language definitions has to > > be ready to dance with G�del, decidability issues and the whole nine > > yards. ANY compiler for a reasonable programming language, and even for > > some unreasonable ones runs right straight into G�del's proof. It > > either does not accept some legal programs, accepts some illegal > > programs, or never halts for some inputs. > > Where do you get this curious idea about G�del's proof? Why do you call that reference to G�del's proof "curious"? I think that it is quite natural (although certainly imprecise and to some degree metaphorical, but it can't be otherwise here) mapping of the sense of that G�del's theorem to the reality of general-purpose programming languages. Or you imply that theorems of (mathematical) logic can't have a sense and therefore shouldn't be mapped to reality at all? -:) Alexander Kopilovitch aek@vib.usr.pu.ru Saint-Petersburg Russia