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,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.50.108.42 with SMTP id hh10mr699964igb.4.1448455538257;
        Wed, 25 Nov 2015 04:45:38 -0800 (PST)
X-Received: by 10.182.148.165 with SMTP id tt5mr437074obb.20.1448455538240;
 Wed, 25 Nov 2015 04:45:38 -0800 (PST)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!news.glorb.com!mv3no2225115igc.0!news-out.google.com!f6ni13133igq.0!nntp.google.com!mv3no2225106igc.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Wed, 25 Nov 2015 04:45:38 -0800 (PST)
In-Reply-To: <176k4qaseow2w.1cckz2yfyq3m2.dlg@40tude.net>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=97.123.238.101;
 posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC
NNTP-Posting-Host: 97.123.238.101
References: <d6318f11-df2c-49bd-928c-2abb766f9c9a@googlegroups.com>
 <n2tddf$eue$1@dont-email.me> <z1z0lmyfw8oz.11i1vv0zjj8ur$.dlg@40tude.net>
 <lyy4dn3d4r.fsf@pushface.org> <1pl8set3ocirg.1v92rqtxaoq3z$.dlg@40tude.net>
 <69b11711-7f19-4b0f-9a5e-66b873a72cc2@googlegroups.com>
 <176k4qaseow2w.1cckz2yfyq3m2.dlg@40tude.net>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <0878b65a-dd37-4f30-a49c-2f2e41c06f6a@googlegroups.com>
Subject: Re: GNAT.Serial_Communication and Streams
From: Shark8 <onewingedshark@gmail.com>
Injection-Date: Wed, 25 Nov 2015 12:45:38 +0000
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Xref: news.eternal-september.org comp.lang.ada:28538
Date: 2015-11-25T04:45:38-08:00
List-Id: <comp.lang.ada>

On Wednesday, November 25, 2015 at 1:52:46 AM UTC-7, Dmitry A. Kazakov wrot=
e:
>=20
> You can validate compilers only against mandated behavior. Stream attribu=
te
> to produce same sequences of stream elements across all Ada compilers is
> just not required.

That's rather irrelevant: that Stream'Input is allowed to have an implement=
ation-defined representation for its stream is immaterial to your claim tha=
t the compiler cannot be verified [as correct, via proof] in-general. It's =
along the same lines as someone saying that a program which is never run ca=
nnot be proven correct, an obvious fallacy.

That there might be errors in the compiler, or that the language might not =
otherwise exist, are not germane to the actual proof. Neither do alternate =
representations necessarily invalidate the compiler... or are you going to =
claim that e.g. a one's-complement computer cannot have a verified Ada comp=
iler because internally the [internal] representation of the integers would=
 be different?