final tuning of unsafe blog post, and publish it

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 390ff51d7de1dae251cefcb7de581ac6b85f4850..6c69d0970e524d3b7377e9e992f4a06779e4b89c 100644 (file)
--- 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 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 %}
 
 Imagine we define another type in our Rust program:
 {% highlight rust %}


@@ -89,7 +89,7 @@ impl MyType<T> {
 {% 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.
 {% 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.
 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:
 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.
 (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.
 
 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`.
 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.
 ## 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?
 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.
 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.
 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.)
 
 (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.)
 
 
 Watch this space, a link to such a post will eventually appear. (And I hope I don't have to write it myself.)