[pjc50]

I think the usual context just requires language soundness; it doesn't depend on having an MMU or anything like that. In particular, protection against:

- out-of-bounds on array read/write

- stack corruption such as overwriting the return address

It doesn't directly say "you can't use C", but achieving this level of soundness in C is quite hard (see sel4 and its Coq proof).

[chillingeffect]

Everyone picks on C, but we have a standard for this. We've been following it for decades in regulated industries. If people take the time, it can be perfectly safe. It requires thinking of a computer as a precision machine, rather than a semantic "do what i'm thinking" box.

[timw4mail]

The problem is that people are really bad at that kind of precision.

[AnimalMuppet]

Maybe I lack vision in such matters, but: how would you corrupt the stack without an out-of-bounds write?

But there's another aspect that I think you missed: use after free.

As you say, achieving this level of soundness with C is hard. Proving it is much harder. (Except, how do you know you've achieved it if you don't prove it?)

[GoblinSlayer]

I suspect seL4 could be proven correct only because it uses simple lifetime patterns.

[milesrout]

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]

> 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.