Hubert Feyrer wrote:

> On Fri, 14 Sep 2001, Lennart Augustsson wrote:
> > No, it's much more powerful.  With a signed driver you have to trust that
> > whoever signed it is not lying (volontary or involontary).  With a proof that
> > YOU check you only have to trust your own proof checking ability.
> > There is no need to trust anyone else, so it is strictly more powerful
> > (and also more difficult to implement).
>
> Right, but as far as I understand, doing such a check would mean to
> analyze the whole (machine) code, automatically, and make some assertion
> if it's "good" or "bad". Sounds tough. :-)

Well, you have to distinguish between who does the tough work and the
easy work.  Yes, it might tough work coming up with a proof that the code
is safe (but with the right code it can be much easier than you might think).
It's easy work to check that the proof is correct.
So the user of the code does the easy work, the proof checking.

    -- Lennart