4 ms·
It might not be just reddit though. The author's summary points to a volatile combination of elements in Rust itself: 1) [T]he Rust project saw Rust as more t
by stanferder 7y ago
It might not be just reddit though. The author's summary points to a volatile combination of elements in Rust itself:
1) [T]he Rust project saw Rust as more than just the language...
2) unsafe... is a really important part of Rust, but also a very dangerous one, hence the name.
If a project is considered to be not just a project, but something closer to a cause, people are going to defend their understanding of that cause fervently.
And introducing the language of "safe" and "unsafe" isn't just descriptive, it's a value judgment. It has connotations of recklessness at least, and explicit threat at worst.
People who perceive themselves to be defending a cause against danger are going to react very strongly, much more so than people who are criticizing an implementation choice on purely technical grounds.
- samatman 7y agoRust didn’t introduce this language, they adopted it. Memory safety has been called that as long as I’ve been programming. Using the antonym of safe was a natural move, though with the benefit of hindsight, `danger` would have been a better keyword. After all, good unsafe code isn’t unsafe! It is dangerous though, because it forgoes guarantees of memory and resource safety provided by the compiler.
- cle 7y ago> And introducing the language of "safe" and "unsafe" isn't just descriptive, it's a value judgment. It has connotations of recklessness at least, and explicit threat at worst. Is it really a value judgment? Coming from a formal PL background, I had just assumed that the "unsafe" keyword was referring to the PL concept of "safety", AKA "soundness", which has a specific technical definition, and not that it was necessarily a value judgment. In that context, "unsafe" just means "the compiler can't guarantee the behavior that it can normally guarantee".
- steveklabnik 7y agoYou are correct. That doesn't mean that people will incorrectly interpret it, though.
- henrikeh 7y agoAda’s language is probably clearer and less loaded: checked and unchecked.
- steveklabnik 7y agoYeah, and interestingly, a lot of unsafe functions use "unchecked" in their names. The issue was that by the time this was recognized, there was too much Rust code, and there was no clear alternative that people universally liked. This kind of conversation is the definition of bikeshedding. I submitted an RFC and it... didn't go well. (I think I picked "trustme" though.)
- cle 7y agoI don't think it's bikeshedding. It does seem to be contributing to the dogmatism I'm seeing from the Rust community here, and this community reaction is a huge problem for Rust. So it matters.
- steveklabnik 7y agoBike shedding is a structural description, not a value judgement. It’s about technical complexity, and changing a keyword is one of the most minimally complex bits of language design.
- cle 7y agoMy point isn't to argue over the definition of bike shedding. If the name of this keyword is contributing to this undesirable community outburst, then its name matters, and discussions about its name are important. That's all I'm saying. If that's what you originally meant, then we are on the same page :).
- steveklabnik 7y agoWe are on the same page, yes.
- stanferder 7y agoPoints well taken, but I think "unsafe" turns it into a value judgment, especially (as samatman says adjacent) since it isn't necessarily really unsafe.
- cle 7y agoIt is unsafe. There are just multiple definitions of unsafe being used here. I agree that it's unfortunate that the meaning of the keyword is easy to misinterpret. Given the background of the people who designed Rust, I don't think it's reasonable to just assume that the keyword "unsafe" has an implicit value judgment.
- Conan_Kudo 7y agoIt absolutely includes value judgement. You just described a form of value judgement too. You're saying that predictable generated code behavior is preferred to unpredictable generated code behavior.
- fluffything 7y ago> And introducing the language of "safe" and "unsafe" isn't just descriptive, it's a value judgment. `unsafe` is a PL term that refers to _soundness_. In Rust, an `unsafe { ... }` block is required to perform an `unsafe` operation, and it precisely means "The code in this block has been proven _sound_". If the code in the block turns out to be _unsound_, e.g., because the proof is incorrect, or non-existent, then the whole program is unsound, and there is nothing that can be said about the execution of such program (usually known as "the execution exhibits undefined behavior"). For example, the Rust compiler has a lint that requires you to write a soundness proof on every `unsafe { ... }` block, explaining why that is sound, and all changes to the compiler are gated on that. In your own projects, you can obviously do whatever you want, but for any non-trivial amount of unsafe code, without a proof, you are basically just building castles in the air.
- rowanG077 7y agoThat's an interesting way too look at it. But that's not how it works in practice. Almost no one in industry is going to write proofs for their unsafe code. It didn't happen for C or C++ and it won't happen for Rust.
- dthul 7y agoIn Rust you at least know where to look at, whereas in C/C++ all code can be "unsafe". With that said, writing unsafe Rust is much easier to screw up than C/C++, since you have to uphold more invariants in unsafe Rust than in C to avoid UB (like never having two mutable references to the same thing at the same time. The very issue which was raised in the actix repository)
- fluffything 7y agoThis is how it works in practice for the Rust compiler for the Rust standard library, and for a lot of foundational crates in crates.io. (Pretty much every well reviewed crate in cargo crate review either does this, or does not contain any unsafe code at all). We also have tools that change for this for very large projects (e.g. cargo-geiger), and tools that help you test your proofs (e.g. cargo-miri). For some unsafe components, there are also proofs in Coq, and the proof systems for Rust unsafe code are making a lot of progress in both defining the rules that unsafe code must uphold in the unsafe-code-guidelines and the Rust spec, as well as in providing example proofs and a standard library of theorems that you can reuse for your own proofs.