add Coq typeclass index problem draft

[web.git] / personal / _posts / 2017-07-17-types-as-contracts.md

diff --git a/personal/_posts/2017-07-17-types-as-contracts.md b/personal/_posts/2017-07-17-types-as-contracts.md
index d7b1b71a54c6dfbdc236bb1a5bf7fe2978f002ce..10a8e4c2f8ae3134d45d4abe46a62d0c844a6c5d 100644 (file)
--- a/personal/_posts/2017-07-17-types-as-contracts.md
+++ b/personal/_posts/2017-07-17-types-as-contracts.md
@@ -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.