move twinsem paper to new folder

[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 59a318b3ac1226b3fdcc1bbd907b893b4396f92d..967b4a3e1b907d590bb661117b79488b1cda3f91 100644 (file)
--- a/personal/_posts/2016-01-09-the-scope-of-unsafe.md
+++ b/personal/_posts/2016-01-09-the-scope-of-unsafe.md
@@ -2,6 +2,8 @@
 title: The Scope of Unsafe
 categories: research rust
 reddit: /rust/comments/4065l2/the_scope_of_unsafe/
+license: CC BY-SA 4.0
+license-url: https://creativecommons.org/licenses/by-sa/4.0/
 ---
 
 I'd like to talk about an important aspect of dealing with unsafe code, that still regularly seems to catch people on the wrong foot:
@@ -11,10 +13,10 @@ I'd like to talk about an important aspect of dealing with unsafe code, that sti
 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).
+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]({% 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.
+**Update (2016-01-11):** Clarified the role of privacy; argued why `evil` is the problem.
 
 <!-- MORE -->
 
@@ -101,7 +103,7 @@ The two types are *syntactically* equal, and the same goes for the two `evil` fu
 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.
+Remember that in a [previous blog post]({% 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.
 
 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.
@@ -157,7 +159,7 @@ 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.
 
-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.
+This should not be entirely surprising if you read the aforementioned [post about formalizing Rust's type system]({% 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.
 
 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.