Re: Ada.Strings.Bounded

Eric Hughes wrote:

> Finally, in order for this to work, you have to be able to connect
> execution of the high-level program with execution of a program of
> equivalent effect in the execution model.  This is where that Hoare
> paper that I mentioned a while back, "Proof of correctness of data
> representations" comes in.  It describes exactly how this works.

Thanks for the title. I see that some methods are actually
heading in this direction. Hopefully, the basic idea that
data and timing must be formally correct, too, finds its way
into education.