3 ms·

Yet that is not what memory safety means. A program being memory safe or not depends on its actual behaviour not what you can prove about that behaviour. There

Yet that is not what memory safety means. A program being memory safe or not depends on its actual behaviour not what you can prove about that behaviour. There are plenty of safe C programs and plenty of unsafe ones. Proving something is safe doesnt make it safe. Also these properties are a very small subset of general correctness. Who cares if you write a "safe" program if it computes the wrong answer?

pjc50 2y ago
> 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 2y ago
  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 2y ago
  Reread my comment. You are confusing proof and fact.