add lang attributes

[web.git] / personal / _posts / 2018-04-05-a-formal-look-at-pinning.md

diff --git a/personal/_posts/2018-04-05-a-formal-look-at-pinning.md b/personal/_posts/2018-04-05-a-formal-look-at-pinning.md
index 2e72c2a6a73f3a7ef004bf939872c642257a4fb5..121de4b1f3401f8feede4bcd3402d942d6b2657c 100644 (file)
--- a/personal/_posts/2018-04-05-a-formal-look-at-pinning.md
+++ b/personal/_posts/2018-04-05-a-formal-look-at-pinning.md
@@ -15,7 +15,7 @@ But before we get started, I have to lay down some basics.
 
 ## Rust types: Recap
 
 
 ## Rust types: Recap
 

-I have discussed my model of Rust types [in a previous post]({{ site.baseurl }}{% post_url 2018-01-31-sharing-for-a-lifetime %}); this may me a good time to read that post as I will be using it as a starting point.
+I have discussed my model of Rust types [in a previous post]({% post_url 2018-01-31-sharing-for-a-lifetime %}); this may me a good time to read that post as I will be using it as a starting point.

 The short version is that I view Rust types with private invariants as not having just a single invariant, but different invariants that reflect the different "modes" the type can be in.
 @cramertj suggested to use "typestate" as terminology here, and I agree that this makes sense.
 
 The short version is that I view Rust types with private invariants as not having just a single invariant, but different invariants that reflect the different "modes" the type can be in.
 @cramertj suggested to use "typestate" as terminology here, and I agree that this makes sense.
 


@@ -34,7 +34,7 @@ The short version is that I view Rust types with private invariants as not havin
 You may be wondering why sharing is a separate typestate here; shouldn't that just be read-only access to a `T` that someone else owns?
 However, that clearly doesn't work for `&Cell`; to explain types with interior mutability we *need* sharing as a separate state.
 I explained this in more detail in the previous post, but as a quick example consider that, if you fully own a `RefCell`, the first field (storing the current count of readers/writers) has no special meaning whatsoever.
 You may be wondering why sharing is a separate typestate here; shouldn't that just be read-only access to a `T` that someone else owns?
 However, that clearly doesn't work for `&Cell`; to explain types with interior mutability we *need* sharing as a separate state.
 I explained this in more detail in the previous post, but as a quick example consider that, if you fully own a `RefCell`, the first field (storing the current count of readers/writers) has no special meaning whatsoever.

-This is witnessed by [`RefCell::get_mut`](https://doc.rust-lang.org/beta/std/cell/struct.RefCell.html#method.get_mut) ignoring that field.
+This is witnessed by [`RefCell::get_mut`](https://doc.rust-lang.org/stable/std/cell/struct.RefCell.html#method.get_mut) ignoring that field.

 In fact, it would be sound to add a `RefCell::reset(&mut self)` that just resets this field to `0`.
 
 ## Pinning
 In fact, it would be sound to add a `RefCell::reset(&mut self)` that just resets this field to `0`.
 
 ## Pinning


@@ -111,7 +111,7 @@ In contrast, converting `Box<T>` to `PinBox<T>` is fine because this *consumes*
 `Pin` lets us give a type to `SelfReferantial` that makes it safe to use.
 This is in the best tradition of Rust: We are using an expressive type system to provide safe APIs for operations that only have unsafe APIs in other languages (e.g., iterators that avoid iterator invalidation which plague even memory safe languages like Java).
 In the following, I will explain how one can prove that our claim of safe encapsulation actually holds true.
 `Pin` lets us give a type to `SelfReferantial` that makes it safe to use.
 This is in the best tradition of Rust: We are using an expressive type system to provide safe APIs for operations that only have unsafe APIs in other languages (e.g., iterators that avoid iterator invalidation which plague even memory safe languages like Java).
 In the following, I will explain how one can prove that our claim of safe encapsulation actually holds true.

-This is building on the framework that we developed for the [RustBelt paper]({{ site.baseurl }}{% post_url 2017-07-08-rustbelt %}).
+This is building on the framework that we developed for the [RustBelt paper]({% post_url 2017-07-08-rustbelt %}).

 
 ## Formal Notation
 
 
 ## Formal Notation