[ryacko]

The theory is simple. I'm somewhat inclined to think it is not so easily applicable.

It is easy to make a secure coprocessor, since the formal logic proofs aren't for such a long set of code.

The fact that rootkits are even possible, that without malware that doesn't involve an elaborate rewrite of the kernel, shows how terrible everything is.

If I didn't know any better, I'd say that Intel is hiring the designers who thought Internet Explorer should be in the kernel.