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-14 14:30:17 PST
Path: 
 archiver1.google.com!news2.google.com!news.maxwell.syr.edu!news2.telebyte.nl!news.cambrium.nl!news.cambrium.nl!news.cambrium.nl!fi.sn.net!newsfeed2.fi.sn.net!newsfeed.kolumbus.fi!not-for-mail
From: Aatu Koskensilta <aatu.koskensilta@xortec.fi>
Newsgroups: comp.lang.ada
Subject: Re: Certified C compilers for safety-critical embedded systems
Date: Thu, 15 Jan 2004 00:52:03 +0200
Organization: Elisa Internet customer
Message-ID: <bu4ftj$g0r$1@phys-news1.kolumbus.fi>
References: <NlSMb.1401$ZG5.733@reader1.news.jippii.net>
 <mailman.0.1074032309.303.comp.lang.ada@ada-france.org>
 <0F6Nb.1623$Tt.642@reader1.news.jippii.net>
 <bu3dr0$1o6$1@a1-hrz.uni-duisburg.de> <TZudnRercMyd75jdRVn-gQ@comcast.com>
NNTP-Posting-Host: 212-246-60-38.adsl.tpo.fi
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 8bit
X-Trace: phys-news1.kolumbus.fi 1074119416 16411 212.246.60.38 (14 Jan 2004
 22:30:16 GMT)
X-Complaints-To: abuse@kolumbus.fi
NNTP-Posting-Date: Wed, 14 Jan 2004 22:30:16 +0000 (UTC)
User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.2.1) Gecko/20030225
X-Accept-Language: en-us, en
In-Reply-To: <TZudnRercMyd75jdRVn-gQ@comcast.com>
Xref: archiver1.google.com comp.lang.ada:4414
Date: 2004-01-15T00:52:03+02:00
List-Id: <comp.lang.ada>

Robert I. Eachus wrote:
> Also, keep in mind that most Ada compilers will accept very large G�del 
> numbers, written in factored form or as constants with hundreds of 
> digits.  You can design a program so that it only accepts a program as 
> legal Ada if a particular G�del number specifies a true theorem in 
> G�del's formalization, and will reject it otherwise.  

I'm not sure if I understand you correctly here - the part where you say 
"You can design a program so that it only accepts a program as
legal Ada if a particular G�del number specifies a true theorem" 
confuses me. Are you saying that for any Pi_1 (#) formula \phi there is 
a standard Ada program \phi*, s.t. \phi* is legal Ada if and only if 
\phi is true (the transformation * being recursive)? Do you have a 
reference for this result? And why do you think this is true for all 
reasonable programming languages?

(#) Surely this is not the case for arbitrary formulae? If it is, Ada 
seems rather an odd language; I've never encountered an actually used 
computer language with correctness of a program not arithmetic.

-- 
Aatu Koskensilta (aatu.koskensilta@xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus