There is another way to phrase the intuition of types having additional invariants:
-> *There is more to types like `Vec` than their definition gives away*.
+> *There is more to types like `Vec` than their syntactic definition gives away*.
Imagine we define another type in our Rust program:
{% highlight rust %}
{% endhighlight %}
This type *looks* exactly like `Vec`, doesn't it?
The two types are *syntactically* equal, and the same goes for the two `evil` functions.
-Still, `MyType::evil` is a perfeclty benign function (despite its name).
+Still, `MyType::evil` is a perfectly benign function (despite its name).
How can this be?
Remember that in a [previous blog post]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}), I argued that types have a *semantic* aspect.
In order to formally describe what it means to be a `Vec`, we can't just say "well, that's a `struct` with these three fields".
That would be *wrong*.
But still, that's actually all the Rust compiler knows, and it is all that it actually checks:
-When type checking `Vec::evil`, the compiler *thinks* that `Vec` is like `MyType`, and under that assumption, it deems `evil` a good function.
+When type checking `Vec::evil`, the compiler *thinks* that `Vec` is like `MyType`, and under that assumption, it deems `evil` a good function in both cases.
(Clearly, the compiler did not watch enough movies with serious villains.)
In other words, we have to look beyond the mere syntactic appearance of a type, and into its deeper, semantic meaning.
As part of my work on formalizing Rust, I will eventually want to prove the soundness of types like `Vec` or `RefCell` and their associated operations.
In order to do so, I will first have to figure out what exactly the semantics of these types are. (This will be fairly easy for `Vec`, but really hard for `RefCell`. Can you guess why?)
Then I will have to check *every* function operating on these types and prove that they are actually well-typed.
+
+The compiler, however, cannot guess or check the actual semantics of `Vec`, the additional invariants we came up with; and this can make seemingly safe code like `Vec::evil` become unsafe.
Even if the Rust compiler says "yup, that function over there is fine, I checked every single statement of it", that's not enough because the Rust compiler has no idea about which types these functions are *actually* about.
All it sees is the syntactic surface.
-While proving soundness of `Vec`, it would then turn out that `Vec::evil` is actually not a semantically well-typed function. It may leave an invalid `Vec` in `self`.
+While proving soundness of `Vec`, it would then turn out that `Vec::evil` is actually not a semantically well-typed function.
+It will invalidate `self`, such that is is no longer an instance of the *actual* (semantic) type `Vec`.
This is just as bad as a function assigning `*f = 42u32` to a `f: &mut f32`.
The difference between `Vec` and `MyType` is no less significant than the difference between `f32` and `u32`.
It's just that the compiler has been specifically taught about `f32`, while it doesn't know enough about the semantics of `Vec`.
## The actual scope of unsafe
At this point, you may be slightly worried about the safety of the Rust ecosystem.
-I just spent two sections arguing that the Rust compiler actually dosn't know what it is doing when it comes to checking functions that work on `Vec`.
+I just spent two sections arguing that the Rust compiler actually doesn't know what it is doing when it comes to checking functions that work on `Vec`.
How does it come that people carelessly use `Vec` in their programs without causing havoc all the time?
-Or, to put it slightly differently: If the scope of `unsafe` grows beyond the syntactc `unsafe` blocks, then how far does it reach?
+Or, to put it slightly differently: If the scope of `unsafe` grows beyond the syntactic `unsafe` blocks, then just how far does it reach?
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.
We may call this *abstraction safety*.
Many type systems have this property, just think of `private` fields in Java or C++, or opaque signatures in ML.
However, few languages embrace using unsafe primitives and encapsulating them behind a layer of abstraction as much as Rust does.
-In some sense, Rust relies way more on abstraction safety than most languages -- though in practice, programmers of all languages rely on abstraction safety a lot, if it is available.
+In some sense, Rust relies way more on abstraction safety than most languages -- though in practice, programmers of all languages rely on abstraction safety a lot, *if* it is available.
(Most scripting languages, I am looking at you.)
-Abstraction safety is a very deep point that deserves its own blog post, I only skimmed the surface.
+Abstraction safety is a very deep point that deserves its own blog post, I only skimmed the surface here.
Watch this space, a link to such a post will eventually appear. (And I hope I don't have to write it myself.)
projects / web.git / commitdiff