[pjc50]

> Proving something is safe doesnt make it safe.

Err .. that is actually the point of the proof. Can you give an example of something with a Coq-type safety proof that has a memory safety bug in it?

[baq]

Not OP but you can in theory add cosmic rays, rowhammer attacks and brownout/undervolt glitching into the mix. Kinda stretching it but sometimes you have to think about these.

[milesrout]

Reread my comment. You are confusing proof and fact.