|
|
|
|
|
|
by SassyThrowaway
1411 days ago
|
|
|
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? |
|
|
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