From 872d0e5214b2bc3b86c38d1d26e08b8aa3b9e0e8 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 9 Jan 2016 13:34:22 +0100 Subject: [PATCH] final tuning of unsafe blog post, and publish it --- .../2016-01-09-the-scope-of-unsafe.md} | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) rename personal/{_drafts/the-scope-of-unsafe.md => _posts/2016-01-09-the-scope-of-unsafe.md} (92%) diff --git a/personal/_drafts/the-scope-of-unsafe.md b/personal/_posts/2016-01-09-the-scope-of-unsafe.md similarity index 92% rename from personal/_drafts/the-scope-of-unsafe.md rename to personal/_posts/2016-01-09-the-scope-of-unsafe.md index 390ff51..6c69d09 100644 --- a/personal/_drafts/the-scope-of-unsafe.md +++ b/personal/_posts/2016-01-09-the-scope-of-unsafe.md @@ -69,7 +69,7 @@ But we are not done yet, we can actually use this observation to learn more abou 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 %} @@ -89,7 +89,7 @@ impl MyType { {% 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. @@ -102,17 +102,20 @@ In other words, the additional invariants that we associate with `Vec` actually 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`. @@ -120,9 +123,9 @@ It's just that the compiler has been specifically taught about `f32`, while it d ## 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. @@ -151,10 +154,10 @@ We rely on the fact that the type system lets us build abstraction boundaries th 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.) -- 2.30.2