I think we'll be able to just prove the correctness of our contracts and then use them safely. Of course you can't do that with Microsoft Windows because it's too complicated, but you can do it with small contract bytecodes.