clarify extra-hidden-state-in-memory

[web.git] / ralf / _posts / 2018-01-31-sharing-for-a-lifetime.md

diff --git a/ralf/_posts/2018-01-31-sharing-for-a-lifetime.md b/ralf/_posts/2018-01-31-sharing-for-a-lifetime.md
index 0b7a4549a886f778204471fb34435b6f31e51362..3a8af093f353182f273d4d1360410b300fe6c729 100644 (file)
--- a/ralf/_posts/2018-01-31-sharing-for-a-lifetime.md
+++ b/ralf/_posts/2018-01-31-sharing-for-a-lifetime.md
@@ -4,11 +4,11 @@ categories: research rust
 forum: https://internals.rust-lang.org/t/sharing-for-a-lifetime/6675
 ---
 
-This post is about an aspect of the [RustBelt paper]({{ site.baseurl }}{% post_url 2017-07-08-rustbelt %}).
+This post is about an aspect of the [RustBelt paper]({% post_url 2017-07-08-rustbelt %}).
 Concretely, I'd like to share some of our thoughts on the nature of types and shared references.
 Let's see how well this goes. :)
 
-Shared references are an extremely powerful mechanism in the Rust type system, and we've had quite some trouble finding a good way of handling them in our [formal model]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}).
+Shared references are an extremely powerful mechanism in the Rust type system, and we've had quite some trouble finding a good way of handling them in our [formal model]({% post_url 2015-10-12-formalizing-rust %}).
 In this post, I will present the model that we came up with.
 <!-- MORE -->
 Let's get started by discussing what a "model" of a type looks like, and what's so hard about handling shared references.
@@ -21,7 +21,7 @@ To see how, I will briefly assume that Rust does *not* permit interior mutabilit
 
 ### What's in a Type?
 
-I've already [written]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}) [about]({{ site.baseurl }}{% post_url 2016-01-09-the-scope-of-unsafe %}) the idea of "semantic types", which essentially boils down to the concept that types can impose *additional invariants* on their fields, like `self.cap >= self.len` (for `Vec`) or `!is_zero(self.0)` (for `NonZero`).
+I've already [written]({% post_url 2015-10-12-formalizing-rust %}) [about]({% post_url 2016-01-09-the-scope-of-unsafe %}) the idea of "semantic types", which essentially boils down to the concept that types can impose *additional invariants* on their fields, like `self.cap >= self.len` (for `Vec`) or `!is_zero(self.0)` (for `NonZero`).
 So, whenever I say "(semantic) type", I really mean "a type's (syntactic) definition (aka the data layout) **and** the additional invariants that the module imposes on this type".
 Two types may be syntactically equal but have different invariants, and then clearly casting from one to the other would be horribly unsafe -- so, these would be completely different types despite their syntactic similarity.
 What really matters for a type is the answer to the question: *Given some sequence of bytes, is this sequence a valid inhabitant of the type?*[^1]