It turns out that the underlying reason for this observation is also a nice illustration for the concept of *semantic types* that comes up in my [work on formalizing Rust]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}) (or rather, its type system).
Finally, this discussion will once again lead us to realize that we rely on our type systems to provide much more than just type safety.
+**Update (Jan 11th):** Clarified the role of privacy; argued why `evil` is the problem.
+
<!-- MORE -->
## An Example
The function `evil` above violates this invariant, while all the functions actually provided by `Vec` (including the ones that are implemented unsafely) preserve the invariant.
That's why `evil` is the bad guy. (The name kind of gave it away, didn't it?)
+Some will disagree here and say: "Wait, but there is some `unsafe` code in `Vec`, and without that `unsafe` code `evil` would be all right, so isn't the problem actually that `unsafe` code?"
+This observation is correct, however I don't think this position is useful in practice.
+`Vec` with `evil` clearly is a faulty data structure, and to fix the bug, we would remove `evil`.
+We would never even think about changing the `unsafe` code such that `evil` would be okay, that would defeat the entire purpose of `Vec`.
+In that sense, it is `evil` which is the problem, and not the `unsafe` code.
+
This may seem obvious in hindsight (and it is also [discussed in the Rustonomicon](https://doc.rust-lang.org/nightly/nomicon/working-with-unsafe.html)), but I think it is actually fairly subtle.
There used to be claims on the interwebs that "if a Rust program crashes, the bug must be in some `unsafe` block". (And there probably still are.)
Even academic researchers working on Rust got this wrong, arguing that in order to detect bugs in data structures like `Vec` it suffices to check functions involving unsafe code.
Does it sprawl through all our code, silently infecting everything we write -- or is there some limit to its effect?
As you probably imagined, of course there *is* a limit. Rust would not be a useful language otherwise.
-The scope of `unsafe` ends at the next *abstraction boundary*.
-This means that everything outside of the `std::vec` module does not have to worry about `Vec`.
-Due to the privacy rules enforced by the compiler, code outside of that module cannot access the private fields of `Vec`, and hence it cannot tell the difference between the syntactic appearance of `Vec` and its actual, semantic meaning.
+*If* all your additional invariants are about *private* fields of your data structure, then the scope of `unsafe` ends at the next *abstraction boundary*.
+This means that everything outside of the `std::vec` module does not have to worry about `Vec`.
+Due to the privacy rules enforced by the compiler, code outside of that module cannot access the private fields of `Vec`.
+That code does not have a chance to violate the additional invariants of `Vec` -- it cannot tell the difference between the syntactic appearance of `Vec` and its actual, semantic meaning.
Of course, this also means that *everything* inside `std::vec` is potentially dangerous and needs to be proven to respect the semantics of `Vec`.
## Abstraction Safety
If the type system of Rust lacked a mechanism to establish abstraction (i.e., if there were no private fields), type safety would not be affected.
However, it would be very dangerous to write a type like `Vec` that has a semantic meaning beyond its syntactic appearance.
-Since users of `Vec` can accidentally perform invalid operations, there would actually be *no bound to the scope of `unsafe`*.
+All code could perform invalid operations like `Vec::evil`, operations that rely on the assumption that `Vec` is just like `MyType`.
+There would actually be *no bound to the scope of `unsafe`*.
To formally establish safety, one would have to literally go over the entire program and prove that it doesn't misuse `Vec`.
The safety promise of Rust would be pretty much useless.
projects / web.git / blobdiff