twinsem paper: directly link to current location

[web.git] / personal / _posts / 2017-07-14-undefined-behavior.md

diff --git a/personal/_posts/2017-07-14-undefined-behavior.md b/personal/_posts/2017-07-14-undefined-behavior.md
index 8176aaf552e60f7f272fd25936e4d5df564fbdd3..26171ac992ea597aafd92d74ee38cd3b252f044e 100644 (file)
--- a/personal/_posts/2017-07-14-undefined-behavior.md
+++ b/personal/_posts/2017-07-14-undefined-behavior.md
@@ -74,7 +74,7 @@ That is not very satisfying.
 ## Undefined Behavior in Rust
 
 Coming back to Rust, where are we at?
 ## Undefined Behavior in Rust
 
 Coming back to Rust, where are we at?

-Safe Rust is [free from UB]({{ site.baseurl }}{% post_url 2017-07-08-rustbelt %}), but we still have to worry about unsafe Rust.
+Safe Rust is [free from UB]({% post_url 2017-07-08-rustbelt %}), but we still have to worry about unsafe Rust.

 For example, what if unsafe code crafts two aliasing mutable references (something that is prevented in safe Rust) and passes them to our `simple` function?
 This violates the assumptions we made when we reordered the two writes.
 If we want to permit this optimization (which we do!), we have to argue why it cannot change program behavior.
 For example, what if unsafe code crafts two aliasing mutable references (something that is prevented in safe Rust) and passes them to our `simple` function?
 This violates the assumptions we made when we reordered the two writes.
 If we want to permit this optimization (which we do!), we have to argue why it cannot change program behavior.


@@ -91,11 +91,11 @@ I also think that tooling to *detect* UB is of paramount importance, and can hel
 To this end, the specification should be written in a way that such tooling is feasible.
 In fact, specifying a dynamic UB checker is a very good way to specify UB!
 Such a specification would describe the additional state that is needed at run-time to then *check* at every operation whether we are running into UB.
 To this end, the specification should be written in a way that such tooling is feasible.
 In fact, specifying a dynamic UB checker is a very good way to specify UB!
 Such a specification would describe the additional state that is needed at run-time to then *check* at every operation whether we are running into UB.

-It is with such considerations in my mind that I have previously written about [miri as an executable specification]({{ site.baseurl }}{% post_url 2017-06-06-MIR-semantics %}).
+It is with such considerations in my mind that I have previously written about [miri as an executable specification]({% post_url 2017-06-06-MIR-semantics %}).

 
 

-Coming up next on this channel:  During my [internship]({{ site.baseurl }}{% post_url 2017-05-23-internship-starting %}), I am working on such a specification.
+Coming up next on this channel:  During my [internship]({% post_url 2017-05-23-internship-starting %}), I am working on such a specification.

 My ideas are concrete enough now that I can write down a draft, which I will share with the world to see what the world thinks about it.
 
 My ideas are concrete enough now that I can write down a draft, which I will share with the world to see what the world thinks about it.
 

-**Update:** [Writing down has happened]({{ site.baseurl }}{% post_url 2017-07-17-types-as-contracts %}).
+**Update:** [Writing down has happened]({% post_url 2017-07-17-types-as-contracts %}).

 
 **Update:** Clarified "Shifting Responsibility".
 
 **Update:** Clarified "Shifting Responsibility".