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 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-16 00:05:13 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!news.tele.dk!news.tele.dk!small.news.tele.dk!news-stoc.telia.net!news-stoa.telia.net!telia.net!nntp.inet.fi!inet.fi!feeder1.news.jippii.net!reader1.news.jippii.net!53ab2750!not-for-mail From: Aatu Koskensilta User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.5) Gecko/20030925 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: Date: Fri, 16 Jan 2004 10:07:05 +0200 NNTP-Posting-Host: 195.74.11.141 X-Complaints-To: newsmaster@saunalahti.com X-Trace: reader1.news.jippii.net 1074240263 195.74.11.141 (Fri, 16 Jan 2004 10:04:23 EET) NNTP-Posting-Date: Fri, 16 Jan 2004 10:04:23 EET Organization: Saunalahti Customer Xref: archiver1.google.com comp.lang.ada:4453 Date: 2004-01-16T10:07:05+02:00 List-Id: Alexandre E. Kopilovitch wrote: > Aatu Koskensilta wrote: > >>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. 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? > 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. G�del's theorem - again, the Halting Problem seems much more appropriate here - 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. Otherwise, since G�del's theorem says nothing about the intricacies of compiler technology, it's simply irrelevant. Is there a reason to speak about G�del's theorem instead of the undecidability of Halting Problem here? >>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. 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. Otherwise Halting Problem tells you nothing about the situation. >>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 -:) I have no such opinions. -- Aatu Koskensilta (aatu.koskensilta@xortec.fi) "Wovon man nicht sprechen kann, daruber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus