Re: GNAT.Serial_Communication and Streams

[Shark8 <onewingedshark@gmail.com>]

On Wednesday, November 25, 2015 at 1:52:46 AM UTC-7, Dmitry A. Kazakov wrote:
> 
> You can validate compilers only against mandated behavior. Stream attribute
> 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 implementation-defined representation for its stream is immaterial to your claim that 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 cannot 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 compiler because internally the [internal] representation of the integers would be different?