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