Alleged "microkernel mathematically proven to be bug free"

[Georgi Guninski]

On Mon, Jul 28, 2014 at 07:04:05PM +0200, Lodewijk andré de la porte wrote:
> 2014-07-28 18:35 GMT+02:00 Georgi Guninski <guninski at guninski.com>:
> 
> > > I have a rough outline for a "cloud computing grid" that verifiably:
> >
> > verifiably? _really_ provable stuff is a very scarce resource IMHO
> > (especially in crypto. do you need crypto? Do you need P \ne NP?).
> >
> 
> Yes, it needs crypto. I said verifably because "proving" an untamperable
> hardware box (IOW: you can only plug it in, nothing else) is what the spec
> says it is, is, well, impossible.
>

Don't think what you wish is possible, but
don't mind you dreaming :)

IIRC _theoretically_ it is possible to run
trusted program on untrusted hardware
with the catch that you need some additional
"proof" - this was a paper can't find at the
moment.