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-16 18:14:33 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!newsfeed.icl.net!newsfeed.fjserv.net!newsfeed.icl.net!newsfeed.fjserv.net!proxad.net!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: Sat, 17 Jan 2004 05:07:16 +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 1074305217 86281 80.67.180.195 (17 Jan 2004 02:06:57 GMT) X-Complaints-To: usenet@melchior.cuivre.fr.eu.org NNTP-Posting-Date: Sat, 17 Jan 2004 02:06:57 +0000 (UTC) To: comp.lang.ada@ada-france.org Return-Path: In-Reply-To: ; from Aatu Koskensilta at Fri, 16 Jan 2004 10:07:05 +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:4477 Date: 2004-01-17T05:07:16+03:00 Aatu Koskensilta wrote: > > G�del's theorem here is not a foundation or cause, but an explanation of > > a fact from reality, which was observed many times. > > G�del's theorem is an explanation of what fact? That compilers tend not > to be correct? How would G�del's theorem explain that fact? In short words, real compilers are under high stress, imposed on them by rich and complex languages, which strive to provide a comprehensive set of features for a programmer (that is, expressive power) and at the same time to satisfy various requirements like portability, convenience of maintenance, etc. (that is, one or another kind of generalization/propagation). Is this stress inevitable? G�del's theorem says: yes, it is inevitable - while you are stuck to these goals. > > 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. > > My knowledge of production-line compilers is not relevant here. Interesting. So, you believe that your knowledge of one thing is irrelevant to your ability to make judgements about its relationship to another thing. > G�del's > theorem - again, the Halting Problem seems much more appropriate here - Seems to you - ok, but note that here you are on foreign territory, it is comp.lang.ada newsgroup, not comp.logic; therefore you if want to be understood, you should provide arguments familiar to native inhabitants. It may be more convenient for you (for any reason) to think in terms of some particular model, but this does not mean that others will share your preferences. > can only be relevant to compilers, if the compilers are thought of as > recursive transformations of programs into programs (in, say, assembly > language) or somehow map into formal theories. Dropping the sacred word "recursive" as inappropriate here, I'd like to inform you that real production-line compilers aren't just transformations of programs into programs, that is, from one formal text to another formal text. First, such a compiler gets at least two input streams, and only one of them is a formal text. Another always present input stream is the stream of programmer's intentions. Any real compiler, even of moderate quality, tries to guess those intentions in many cases/points, and takes them into account. Second, a real compiler produces at least 3 output streams, and again, only one of them is (more or less) formal text. Two other always present streams are diagnostic-errors and diagnostic-warnings, and they aren't formal... even diagnostic-errors isn't. (And "getting there is just a beginning" -;) > Is there a reason to speak about G�del's theorem instead of the > undecidability of Halting Problem here? Certainly yes, because the main problems are not in compilers (algorithms), but in design of languages. > > 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. > > The Halting Problems speaks about recursive functions. In order to make > applications of it to a real world situation, you have to be able to see > some things in the situation as being recursive functions. Recursion means stack, and stack is very human thing, it rarely happens in non human-made reality. Personally, I like priority queues much better -:) . Alexander Kopilovitch aek@vib.usr.pu.ru Saint-Petersburg Russia