make it clear that this is an RSS feed
[web.git] / personal / _posts / 2017-07-17-types-as-contracts.md
index d7b1b71a54c6dfbdc236bb1a5bf7fe2978f002ce..3ef565a4b1eeb3819256b59697ebe34d031e34e6 100644 (file)
@@ -4,14 +4,14 @@ categories: internship rust
 forum: https://internals.rust-lang.org/t/types-as-contracts/5562
 ---
 
-Over the last couple of weeks of my [internship]({{ site.baseurl }}{% post_url
+Over the last couple of weeks of my [internship]({% post_url
 2017-05-23-internship-starting %}), I have been working on a proposal for the "Unsafe Code Guidelines".
 I got some very encouraging feedback at the [Mozilla All-Hands](https://internals.rust-lang.org/t/recapping-this-weeks-mozilla-all-hands/5465),
 and now I'd like to put this proposal out there and start having a discussion.
 <!-- MORE -->
 Warning: Long post is long.  You have been warned.
 
-If you need more context on this topic, I suggest you read my post on [unsafe code guidelines and undefined behavior]({{ site.baseurl }}{% post_url 2017-07-14-undefined-behavior %}) first.
+If you need more context on this topic, I suggest you read my post on [unsafe code guidelines and undefined behavior]({% post_url 2017-07-14-undefined-behavior %}) first.
 
 ## 1 It's in the Types
 
@@ -48,7 +48,7 @@ In particular, `simple` would validate `x` and `y` immediately after being calle
 
 ## 2 Specification Framework
 
-I have [previously written about my thoughts on undefined behavior]({{ site.baseurl }}{% post_url 2017-07-14-undefined-behavior %}):
+I have [previously written about my thoughts on undefined behavior]({% post_url 2017-07-14-undefined-behavior %}):
 
 > I also think that tooling to *detect* UB is of paramount importance [...].
 In fact, specifying a dynamic UB checker is a very good way to specify UB!
@@ -56,8 +56,8 @@ Such a specification would describe the additional state that is needed at run-t
 
 Following this, I will in the following describe how we could check the contracts expressed by Rust's types for violations.
 I am considering a MIR program; if a Rust program is supposed to be checked, it has to be translated to MIR first.
-(You can [read up on my explanation]({{ site.baseurl }}{% post_url 2017-05-23-internship-starting %}) of why I think this is a good way to proceed.)
-The validation of reference types (in particular, their exclusive / read-only nature) will need some extra "instrumented" state -- also see [this previous post on the topic]({{ site.baseurl }}{% post_url 2017-06-06-MIR-semantics %}).[^1]
+(You can [read up on my explanation]({% post_url 2017-05-23-internship-starting %}) of why I think this is a good way to proceed.)
+The validation of reference types (in particular, their exclusive / read-only nature) will need some extra "instrumented" state -- also see [this previous post on the topic]({% post_url 2017-06-06-MIR-semantics %}).[^1]
 The extra state in my proposal consists of something akin to a reader-writer lock for every memory location.
 I am first going to describe these locks and how they affect program behavior, before explaining contract validation.
 
@@ -320,7 +320,7 @@ One topic that needs special treatment in this context is interior mutability.
 If a function takes an `x: &Cell<i32>`, following the rules above, it will acquire a read lock of `*x` for the duration of the function call, making `*x` immutable.
 Clearly, we do not want to do that -- calling `x.set` *will* actually mutate `*x`, and mutating through a shared reference is exactly the point of using `Cell`!
 
-Lucky enough, the compiler *already* says that interior mutability is only allowed via [`UnsafeCell`](https://doc.rust-lang.org/beta/core/cell/struct.UnsafeCell.html).
+Lucky enough, the compiler *already* says that interior mutability is only allowed via [`UnsafeCell`](https://doc.rust-lang.org/stable/core/cell/struct.UnsafeCell.html).
 We can use this for our purposes: To adjust validation for interior mutability, we *stop* our recursive descent and do not do anything when reaching an `UnsafeCell` *while `mutbl` indicates we are in immutable mode* -- `&mut UnsafeCell` is not affected.
 In particular, no locks are acquired.
 This justifies calling `set` on a shared reference and having the value changed.