stress privacy a little more
authorRalf Jung <post@ralfj.de>
Mon, 11 Jan 2016 13:41:58 +0000 (14:41 +0100)
committerRalf Jung <post@ralfj.de>
Mon, 11 Jan 2016 13:41:58 +0000 (14:41 +0100)
personal/_posts/2016-01-09-the-scope-of-unsafe.md

index 995cb61375ed7f3e844a55fe6332bd02daf7be01..403d6b3eab6c6e0f7e477e3a1998666d721334ad 100644 (file)
@@ -130,9 +130,10 @@ Or, to put it slightly differently: If the scope of `unsafe` grows beyond the sy
 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.
 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
 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
@@ -143,7 +144,8 @@ This nicely brings us to another important point, which I can only glimpse at he
 
 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.
 
 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.
 
 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.