On: MiniRust

[SassyThrowaway]

The distintion between Rust and C looks interesting. Are there any formal (or formal-ish) grounds for saying that only authors of unsafe code need to be aware of Undefined Behaviour in Rust? With MiniRust, would it be plausible that some sort of "black-box abstraction" theorem could be proven, in a way that makes "safe" code depending on "unsafe" code insensitive to undefined behaviours?

[ralfj → SassyThrowaway]

> Are there any formal (or formal-ish) grounds for saying that only authors of unsafe code need to be aware of Undefined Behaviour in Rust?

Yes. It's called type safety / type soundness: you cannot cause UB in safe code.

I literally did a PhD on that topic: https://research.ralfj.de/phd/thesis-screen.pdf