4 ms·
This is a very good explanation. It's sad that these terms are so counterintuitive. I still regularly have to clarify the confusion between undefined and unspe
by codeflo 4y ago
This is a very good explanation.
It's sad that these terms are so counterintuitive. I still regularly have to clarify the confusion between undefined and unspecified behavior. And to be fair, "define" and "specify" are basically synonyms in everyday language, it's evil that these terms have so wildly different meanings. Quite a bit of confusion is caused by people not fully understanding that "unsafe" in Rust actually just means "unchecked", i.e. not verified by the compiler, and not necessarily "insecure".
Now we add "unsound" to the mix, and I fear that all of this is simply too hard to learn.
Maybe we should reverse all those terms to be positive, and also use words in their intuitive meaning, and also avoid confusing almost-synonyms. Here's a quick attempt:
1. "Well-behaved" code would be code that only accesses memory correctly. (That's not fully precise enough. What I actually mean of course is "no UB", but that's hard to put into words if you don't already know what UB is. Let's say well-behaved code only does "allowed stuff".)
2. "Checked" code is code verified by Rust's compiler to be well-behaved if certain invariants are fulfilled. Code is always checked by default unless you opt out with a special keyword (confusingly called "unsafe").
3. "Sound" code is well-behaved code (that may or may not be checked by the compiler) with the additional restriction that will remain well-behaved no matter how it's embedded into checked code. This is what enables "safe abstractions". Checked code is automatically sound by this definition, but alternatively, unchecked code could also be sound, which would have to be manually verified somehow. To do this, you obviously need to know which assumptions the checker makes in its reasoning.
(Edit: Reworded a bit to address an unexpected source confusion. What's now called "well-behaved" was called "safe", but that has multiple meanings. Some of the responses in the thread apply to the old version.)
- LegionMammal978 4y agoI don't think your attempt would be quite accurate: safe code, even though it is checked, can cause UB. This can only occur if some earlier unsafe code was unsound, by the current definition. For instance, suppose you have an ordinary Box<i32>. Then, you dereference it to create a local &i32 reference, and use unsafe code to turn it into a &'static i32 reference. Then, you drop the Box<i32>, which deallocates the backing memory. Finally, you attempt to read the value from the &'static i32. The UB occurs only at the last step, when you read from deallocated memory. But reading from a &'static i32 reference is completely allowed in safe, checked code. That's why we use the term "unsound" to cast fault on the earlier unsafe code which allowed us to do this.
- codeflo 4y agoThat's a very good example. I think that's what I meant by: > "Sound" code is safe code (that may or may not be checked by the compiler), that will remain safe no matter how it's called by checked code. Maybe "called" was too specific, it could be embedded in other ways. But it's clear in your example that there's a way of integrating the unsafe cast into otherwise fully checked code that leads to UB. Hence, it is not sound.
- skitter 4y agoJust holding an invalid reference is UB, even if you don't do anything with it (the example still works as the reference gets invalidated by safe code).
- LegionMammal978 4y agoA reference is never really "held": from a language-semantics standpoint, it only exists when it is actually used. In this example, copying, reborrowing, or accessing the reference would be UB, but simply letting it fall out of scope would not be UB (modulo the UCG issue oconnor mentioned; but I personally doubt that this status quo will change). You can try this yourself with Tools > Miri on the Playground (https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=6f829f372fa97bea62ccf7a1ae1c6871 https://play.rust-lang.org/?version=stable&mode=debug&editio...). The distinction is far more relevant for unsafe code than for safe code.
- oconnor663 4y agoI think there are some aspects of this rule that are still undecided. See for example: - https://github.com/rust-lang/unsafe-code-guidelines/issues/84 https://github.com/rust-lang/unsafe-code-guidelines/issues/8... - https://github.com/rust-lang/miri/issues/2732 https://github.com/rust-lang/miri/issues/2732
- oconnor663 4y agoYeah this is a great example of why formally defining "soundness" is so tricky. Not only do we have to worry about unsafe code committing UB, we also have to worry about it setting up a situation where safe code might commit UB later. Soundness is a property of functions and modules, but that property is a statement about the entire program that contains them, or actually about any program that could contain them. In retrospect, I kind of wish I had asked somebody like Ralf Jung to review this post before I published it. On the other hand, the fastest way to get an answer on the internet is to post the wrong answer :-D
- hitekker 4y ago[flagged]
- JeremyBanks 4y ago[dead]
- burntsushi 4y agoAs a former member of the Rust mod team, and a continuing member of the Rust project, this narrative is complete bullshit.
- hitekker 4y agoIt'd be awesome to hear the real narrative around the infighting of Rust's former maintainers and moderators. So far, I've just been watching the sparks fly from the outside. Like your resignation note where the Core Team was alleged to "unaccountable" https://github.com/rust-lang/team/pull/671 https://github.com/rust-lang/team/pull/671 and implied that to be untrustworthy. Or like how maintainers called Zig a "massive step backward" for the industry https://news.ycombinator.com/item?id=32783244 https://news.ycombinator.com/item?id=32783244. Memories change awfully quickly when positions are up in the air though. If there's an investigative report, I'm sure it can settle some of the open questions around nepotism and the downfall of the original leadership https://news.ycombinator.com/item?id=28633113 https://news.ycombinator.com/item?id=28633113.
- burntsushi 4y agoYou're obviously a troll and have already made up your own mind. And I've already said publicly what I'm going to say. So I'm going to take a hard pass buddy. Stop spreading misinformation. Even your comment here where you're "just asking questions" contains a pile of bullshit.
- hitekker 4y agoLabeling the past year as a "troll" is one way to deal with the pain of failure. For the previous maintainers and moderators, giving up on managing Rust and being sidelined from Rust's leadership must have been painful. But it's necessary since they just weren't mature enough nor honest enough to be trusted with Rust.