🚀 go-pugleaf

Debora Weber-Wulff writes:
   [about validating system utilities]

>Well, we're getting there. J Moore did a proof of correctness for an
>assembler, William Bevier did a proof for a small kernel, and Warren
>Hunt did one for the gate level implementation of a chip using the
>Boyer-Moore prover (see Journal of Automated Reasoning, December
>1989). The prover - an obstinate, nagging proof checker that won't
>accept any nonsense - required the proof of all sorts of lemmata that
>get close to your problems. For example, it needed to be proven that
>the assembler program code could not modify itself during execution.

This is fun.

But there is assembler code which modifies itself during execution,
and then there is assembler code which modifies machine code before
execution (linking loaders, loaders in general, debuggers, and
possibly future functional languages).

I'd be interested in hearing how the formalisms worked around those
cases.  (I'm surrounded by libraries, but my schedule makes in hard to
get to any while they're open :-(

Raul Rockwell