papers update: add ICFP talk; add refinement paper

[web.git] / personal / _posts / 2016-01-09-the-scope-of-unsafe.md

diff --git a/personal/_posts/2016-01-09-the-scope-of-unsafe.md b/personal/_posts/2016-01-09-the-scope-of-unsafe.md
index 403d6b3eab6c6e0f7e477e3a1998666d721334ad..757bd738ca155ea2402454551dd0bec225e04eed 100644 (file)
--- a/personal/_posts/2016-01-09-the-scope-of-unsafe.md
+++ b/personal/_posts/2016-01-09-the-scope-of-unsafe.md
@@ -14,6 +14,8 @@ What I am saying is that the scope of `unsafe` is larger than the `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).
 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.
 
 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.
 

+**Update (Jan 11th):** Clarified the role of privacy; argued why `evil` is the problem.
+

 <!-- MORE -->
 
 ## An Example
 <!-- MORE -->
 
 ## An Example


@@ -60,6 +62,12 @@ More precisely speaking, `ptr` points to an array of type `T` and size `cap`, of
 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.
 That's why `evil` is the bad guy. (The name kind of gave it away, didn't it?)
 
 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.
 That's why `evil` is the bad guy. (The name kind of gave it away, didn't it?)
 

+Some will disagree here and say: "Wait, but there is some `unsafe` code in `Vec`, and without that `unsafe` code `evil` would be all right, so isn't the problem actually that `unsafe` code?"
+This observation is correct, however I don't think this position is useful in practice.
+`Vec` with `evil` clearly is a faulty data structure, and to fix the bug, we would remove `evil`.
+We would never even think about changing the `unsafe` code such that `evil` would be okay, that would defeat the entire purpose of `Vec`.
+In that sense, it is `evil` which is the problem, and not the `unsafe` code.
+

 This may seem obvious in hindsight (and it is also [discussed in the Rustonomicon](https://doc.rust-lang.org/nightly/nomicon/working-with-unsafe.html)), 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 (and it is also [discussed in the Rustonomicon](https://doc.rust-lang.org/nightly/nomicon/working-with-unsafe.html)), 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.