Eric Hughes wrote:
> 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.
On Apr 15, 2:33 pm, Georg Bauhaus <rm.tsoh.plus-
bug.bauh...@[EMAIL PROTECTED]
> wrote:
> 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.
You're welcome. That essay is collected in the book _Essays in
Computing Science_.
The title of that essay might well have been titled "Proof of
correctness of compiler output", but Hoare doesn't go into compilation
issues as such in enough depth to justify such a title. You'd have a
program annotated with some properties and their proof, a compiler
that converted the proof to one in its execution model, and proof-
carrying object code as its output. Even if the proof annotations of
the program were empty (as today), you can still infer some basic
semantics from expressions and statements by themselves and generate
checkable proof. I suspect that discipline would get rid of a lot of
code generation defects.
Eric
|
