get rid of category "university"

[web.git] / personal / _drafts / the-scope-of-unsafe.md

diff --git a/personal/_drafts/the-scope-of-unsafe.md b/personal/_drafts/the-scope-of-unsafe.md
index 36c972d2b3fe72b915b0cb9768908f23cb894c40..641b4bb2e86e71e2ba3d5381e82a8574ac7707d0 100644 (file)
--- a/personal/_drafts/the-scope-of-unsafe.md
+++ b/personal/_drafts/the-scope-of-unsafe.md
@@ -7,14 +7,17 @@ I'd like to talk about an important aspect of dealing with unsafe code, that sti
 
 > *When checking unsafe code, it is not enough to just check the contents of every `unsafe` block.*
 
 
 > *When checking unsafe code, it is not enough to just check the contents of every `unsafe` block.*
 

-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).
+The "scope" in the title refers to the extent of the code that has to be manually checked for correctness, once `unsafe` is used.
+What I am saying is that the scope of `unsafe` is larger than the `unsafe` block itself.
+
+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.
 
 <!-- MORE -->
 
 ## An Example
 
 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.
 
 <!-- MORE -->
 
 ## An Example
 

-Before we dive into the deeper reasons for why we have to check (seemingly) safe code, let me start by convincing your that the above statement is actually true.
+Before we dive into the deeper reasons for *why* we have to check (seemingly) safe code, let me start by convincing your that this is actually the case.

 
 Consider the type `Vec`, which is roughly defined as follows:
 {% highlight rust %}
 
 Consider the type `Vec`, which is roughly defined as follows:
 {% highlight rust %}


@@ -47,10 +50,10 @@ So, this example clearly shows that to evaluate the safety of types like `Vec`,
 
 ## The reason why
 
 
 ## The reason why
 

-So, why is it the case that a safe function can break `Vec`?
+Why is it the case that a safe function can break `Vec`?

 How can we even say that it is the safe function which is at fault, rather than some piece of `unsafe` code elsewhere in `Vec`?
 
 How can we even say that it is the safe function which is at fault, rather than some piece of `unsafe` code elsewhere in `Vec`?
 

-The intuitive answer most people will give is that `Vec` has *additional invariants* on its fields.
+The intuitive answer is that `Vec` has *additional invariants* on its fields.

 For example, `cap` must be greater than or equal to `len`.
 More precisely speaking, `ptr` points to an array of type `T` and size `cap`, of which the first `len` elements have already been initialized.
 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.
 For example, `cap` must be greater than or equal to `len`.
 More precisely speaking, `ptr` points to an array of type `T` and size `cap`, of which the first `len` elements have already been initialized.
 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.


@@ -59,10 +62,15 @@ That's why `evil` is the bad guy. (The name kind of gave it away, didn't it?)
 This may seem obvious in hindsight, 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.
 This may seem obvious in hindsight, 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.

+That's why I think it's worth dedicating an entire blog post to this point.
+But we are not done yet, we can actually use this observation to learn more about types and type systems.

 
 ## The semantic perspective
 
 There is another way to phrase the intuition of types having additional invariants:
 
 ## The semantic perspective
 
 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*.
+

 Imagine we define another type in our Rust program:
 {% highlight rust %}
 pub struct MyType<T> {
 Imagine we define another type in our Rust program:
 {% highlight rust %}
 pub struct MyType<T> {


@@ -87,9 +95,9 @@ 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.
 For example, a function is semantically well-typed if it *behaves* properly on all valid arguments, independently of how, *syntactically*, the function body has been written down.
 
 Remember that in a [previous blog post]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}), I argued that types have a *semantic* aspect.
 For example, a function is semantically well-typed if it *behaves* properly on all valid arguments, independently of how, *syntactically*, the function body has been written down.
 

-Semantically speaking, `Vec` is very different from `MyType`:
+The reason for `MyType::evil` being fine, while `Vec::evil` is bad, is that semantically speaking, `Vec` is very different from `MyType` -- even though they look so similar.

 If I have a `Vec`, I actually know that `ptr` is valid, that `len <= cap`, and so on.
 If I have a `Vec`, I actually know that `ptr` is valid, that `len <= cap`, and so on.

-I know nothing like that about an arbitrary instance of `MyType`: All I know here is that `cap` and `len` are valid elements of `usize`.
+I know nothing like that about an arbitrary instance of `MyType`: All I have here is that `cap` and `len` are valid elements of `usize`.

 In other words, the additional invariants that we associate with `Vec` actually make this an *entirely different type*.
 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*.
 In other words, the additional invariants that we associate with `Vec` actually make this an *entirely different type*.
 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*.


@@ -103,21 +111,24 @@ In order to do so, I will first have to figure out what exactly the semantics of
 Then I will have to check *every* function operating on these types and prove that they are actually well-typed.
 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.
 Then I will have to check *every* function operating on these types and prove that they are actually well-typed.
 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.

-It would then turn out, for example, that `Vec::evil` is actually not a semantically well-typed function. It may leave an invalid `Vec` in `self`.
-This is just as bad as a function assigning `*b = 42` to a `b: &mut bool`.
-The only difference is that the compiler will catch the second example since it knows all about the semantics of `bool`. It doesn't know enough about the semantics of `Vec`.
+
+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`.
+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`.
 How does it come that people carelessly use `Vec` in their programs without causing havoc all the time?
 
 ## 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`.
 How does it come that people carelessly use `Vec` in their programs without causing havoc all the time?

-Or, to put it slightly different: If the "scope" of `unsafe` (i.e., the code that is potentially "infected" and has to be checked manually) grows beyond the syntactc `unsafe` blocks, then how far does it reach?
-Does it sprawl through all our code, or is there some limit to its effect?
+Or, to put it slightly differently: If the scope of `unsafe` grows beyond the syntactc `unsafe` blocks, then 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: The scope of `unsafe` ends at the next *abstraction boundary*.
+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`.
 This means that everything outside of the `std::vec` module does not have to worry about `Vec`.

-Due to the privacy rules enforces 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.
+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.

 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


@@ -127,19 +138,20 @@ This nicely brings us to another important point, which I can only glimpse at he
 > *The purpose of type systems goes far beyond type safety: They (also) serve to establish safe abstractions.*
 
 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.
 > *The purpose of type systems goes far beyond type safety: They (also) serve to establish safe abstractions.*
 
 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 is actually *no bound to the scope of `unsafe`*.
+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`*.

 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.
 

-This should not be entirely surprising if you read my previous [post about formalizing Rust's type system]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}), where I already argued that a proof of (syntactic) type safety does not help to justify safety of most Rust programs out there.
+This should not be entirely surprising if you read the aforementioned [post about formalizing Rust's type system]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}), where I already argued that a proof of (syntactic) type safety does not help to justify safety of most Rust programs out there.

 I am now making a similar point, coming from a different angle.
 
 I am now making a similar point, coming from a different angle.
 

-The fact that Rust programers *can* use `Vec` and many other types without much care is a property of the type system that is independent of type safety.
-We may call it *abstraction safety*.
+The fact that Rust programmers *can* use `Vec` and many other types without much care is a property of the type system that is independent of type safety.
+We rely on the fact that the type system lets us build abstraction boundaries that cannot be violated by safe code.
+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.
 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 an 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.
+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.

 (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.
 (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.