remove old redirect file

[web.git] / personal / _posts / 2017-05-23-internship-starting.md

diff --git a/personal/_posts/2017-05-23-internship-starting.md b/personal/_posts/2017-05-23-internship-starting.md
index c8283166c6db29e0b25cc569df66d0a9a92f5323..eb523b50fe493537496f2d20c4f831d10ee61e5a 100644 (file)
--- a/personal/_posts/2017-05-23-internship-starting.md
+++ b/personal/_posts/2017-05-23-internship-starting.md
@@ -1,5 +1,5 @@
 ---
 ---

-title: "Day 1 of My Mozilla Internship, or: How to Specify Program Behavior?"
+title: "How to Specify Program (Undefined) Behavior?"

 categories: internship rust
 ---
 
 categories: internship rust
 ---
 


@@ -7,12 +7,14 @@ This summer, I am given the awesome opportunity of spending three months in the
 I am extremely grateful that Mozilla is providing this opportunity to me; hopefully I can give something back by making some hands-on contributions to the Rust ecosystem.
 <!-- MORE -->
 
 I am extremely grateful that Mozilla is providing this opportunity to me; hopefully I can give something back by making some hands-on contributions to the Rust ecosystem.
 <!-- MORE -->
 

+**Update:** This post was originally titled "Day 1 of My Mozilla Internship, or: How to Specify Program Behavior?" but I feel that did not really reflect its content very well. **/Update**
+

 Today is day 1 of my internship -- at least if you start counting at 0, which of course we all do.
 I meant to write this yesterday, but the morning was filled with bureaucratics and in the afternoon I got so jetlagged, I essentially was sleeping with my eyes open.
 (But don't tell Aaron, my manager, or Niko, my mentor -- I was of course supposed to be working. ;)
 
 So, what concretely will I be doing in the next three months?
 Today is day 1 of my internship -- at least if you start counting at 0, which of course we all do.
 I meant to write this yesterday, but the morning was filled with bureaucratics and in the afternoon I got so jetlagged, I essentially was sleeping with my eyes open.
 (But don't tell Aaron, my manager, or Niko, my mentor -- I was of course supposed to be working. ;)
 
 So, what concretely will I be doing in the next three months?

-Based on [my prior posts]({{ site.baseurl }}{% post_url 2016-01-09-the-scope-of-unsafe %}) and me being in the [unsafe code guidelines strike team](https://internals.rust-lang.org/t/next-steps-for-unsafe-code-guidelines/3864) (which I totally forgot to announce here... I'm not good at this blogging thing, am I?), it should not be surprising that my main project is going to be related to unsafe code.
+Based on [my prior posts]({% post_url 2016-01-09-the-scope-of-unsafe %}) and me being in the [unsafe code guidelines strike team](https://internals.rust-lang.org/t/next-steps-for-unsafe-code-guidelines/3864) (which I totally forgot to announce here... I'm not good at this blogging thing, am I?), it should not be surprising that my main project is going to be related to unsafe code.

 More specifically, we want to figure out ways to specify what unsafe code is and what it is not allowed to do (i.e., when its behavior is well-defined, and when it is undefined).
 Ultimately, the way I think this should be specified (and lucky enough, my new bosses agree on this) is by defining, for every possible Rust (or rather, MIR) program one could write, what that program is going to do when it is executed.
 
 More specifically, we want to figure out ways to specify what unsafe code is and what it is not allowed to do (i.e., when its behavior is well-defined, and when it is undefined).
 Ultimately, the way I think this should be specified (and lucky enough, my new bosses agree on this) is by defining, for every possible Rust (or rather, MIR) program one could write, what that program is going to do when it is executed.
 


@@ -29,7 +31,7 @@ And finally, an interpreter can be used for testing:  We could actually check wh
 This will be very important while we are still developing the specification (to check whether our intuition for what should and should not be allowed matches the interpreter), but it is also extremely useful later for authors of unsafe code to check whether they are violating the rules we are going to put in place.
 
 Lucky enough, such an interpreter already exists: [miri](https://github.com/solson/miri)!
 This will be very important while we are still developing the specification (to check whether our intuition for what should and should not be allowed matches the interpreter), but it is also extremely useful later for authors of unsafe code to check whether they are violating the rules we are going to put in place.
 
 Lucky enough, such an interpreter already exists: [miri](https://github.com/solson/miri)!

-That's great, because it means I do not have to write an interpreter from scratch, defining what a stack is and how to perform integers operations and whatnot.
+That's great, because it means I do not have to write an interpreter from scratch, defining what a stack is and how to perform integer operations and whatnot.

 Instead, I can concentrate on the interesting questions coming up in the unsafe code guidelines:
 What exactly do the guarantees "mutable borrows don't have aliases" and "the pointees of shared borrows are not mutated" *mean*?  How should they be reflected in a semantics of MIR -- in miri -- such that the desired [optimizations](https://github.com/nikomatsakis/rust-memory-model/tree/master/optimizations) are actually legal, while at the same time the [unsafe code](https://doc.rust-lang.org/nomicon/) people write has the desired behavior?
 
 Instead, I can concentrate on the interesting questions coming up in the unsafe code guidelines:
 What exactly do the guarantees "mutable borrows don't have aliases" and "the pointees of shared borrows are not mutated" *mean*?  How should they be reflected in a semantics of MIR -- in miri -- such that the desired [optimizations](https://github.com/nikomatsakis/rust-memory-model/tree/master/optimizations) are actually legal, while at the same time the [unsafe code](https://doc.rust-lang.org/nomicon/) people write has the desired behavior?