Hmm. Yeah, that would be a problem, wouldn't it. There are failures that cannot be proven to not occur at compile time, namely, as you mention, hardware errors.

Hmm. Yeah, that would be a problem, wouldn't it. There are failures that cannot be proven to not occur at compile time, namely, as you mention, hardware errors. ECC will prevent some of these, but not all. So perhaps it should still be layered at the hardware level. (Reminds me of the JVM exploit that relied on waiting for random bitflips in RAM.) (Of course, this is a problem for traditional OSs as well, although the vulnerable area of memory (ring0 data structures / stack / etc) is smaller.) I wonder. It might be possible to express some of that in the proof requirements - "this program must not write to memory owned by another process even if a single bitflip occurs anywhere" - although that would probably balloon the complexity of the proof.