Re: GNAT.Serial_Communication and Streams

[Shark8 <onewingedshark@gmail.com>]

On Tuesday, November 24, 2015 at 3:45:52 AM UTC-7, Dmitry A. Kazakov wrote:
> On Tue, 24 Nov 2015 10:28:20 +0000, Simon Wright wrote:
> > I wholly agree with "trust, but verify", though!
> 
> You can verify given compiler for given machine. You cannot do that in
> general.

Whyever not?
Let us suppose that the compiler is represented by a function F(Text) -> Object;
furthermore, let F be a compositional function such that:
function FE(text) -> token_stream
function CP(token_stream) -> intermediate_form
function BE(intermediate_form) -> Object
and
function F = BE(CP(FE))

Now, obviously we can have the front-end take the text (be it in ASCII, EBDIC, or one of the UTF formats) and produce tokens which are a record of [Token_ID, Lexeme] where Lexeme is a standard textual form (let's say UTF32-BE). Now obviously we could split this so that FE = Encode_UTF(Decode_Particular(File)) -- this is to say that, conceptually, the front-end (FE) will only receive the proper UTF32-BE regardless of the particular encoding... nothing here should be dependent on the underlying architecture.

Let us now consider CP*, here we have a function taking a stream of tokens and returning the proper IR; obviously this could be verified and also should be independent of the underlying architecture.

Finally, considering the back-end (BE) we have essentially the same problem as the above CP, with the addition that the execution of the result is correct. So it seems the only possible break in applying verification is the HW/BE divide, that the emitted code /does/ what it is supposed to do, but given that HW manufacturers have used formal methods verification to prove the HW (for some HW), it is certainly possible on the HW level as well.

Going back to the idea of Forth, where every word (Forth's name for function) is defined as a either a list of words or some (usually very small) machine-code to be executed we could define a minimal set of words and implement the rest of Forth's standard dictionary in them --which means that to port the entire [verified] compiler we'd just have to rewrite the aforementioned words, and feed the compiler's source to itself-- this reduces our machine-dependent verification-burden to only the instructions used in that small set of words that all the other words are written in.

So, hooking the idea of having verified IR emition, if we use Forth as our IR then [once the entire compiler is verified] so long as we've verified the instructions used in our minimal dictionary on our new target we have a verified compiler.

Sure it's a lot of work, but I see no reason to consider it impossible.




* -- Arguably CP is the 'heart' of the compiler and can itself be viewed as a series of transformations; and it itself can conceptually be broken down into a aeries of transformations.