thank centril

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

diff --git a/ralf/_posts/2017-05-23-internship-starting.md b/ralf/_posts/2017-05-23-internship-starting.md
index 7a4eea0ad05d0b6a8a76327e8032b01d880aeac1..149b4f38b0401be832e6336c1b29ada0fff7d780 100644 (file)
--- a/ralf/_posts/2017-05-23-internship-starting.md
+++ b/ralf/_posts/2017-05-23-internship-starting.md
@@ -1,5 +1,5 @@
 ---
-title: Day 1 of My Mozilla Internship
+title: "How to Specify Program (Undefined) Behavior?"
 categories: internship rust
 ---
 
@@ -7,6 +7,8 @@ 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 -->
 
+**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. ;)
@@ -37,7 +39,7 @@ That's it for now.
 I don't have the answers to these questions, but hopefully my work will help getting closer to an answer.
 I will keep you posted on my progress (or lack thereof), probably on a weekly or bi-weekly basis.
 
-**Update.** I realized I should probably expand on the parenthetical remark about specifying MIR rather than specifying Rust.
+**Update:** I realized I should probably expand on the parenthetical remark about specifying MIR rather than specifying Rust.
 What we are planning to do here is to specify Rust by specifying (a) how Rust code translates to MIR, and (b) specifying MIR.
 This has two advantages.
 First of all, part (a) actually is already done and implemented in the Rust compiler!
@@ -51,3 +53,4 @@ Now, this is *not* to say that every Rust compiler has to use MIR in its compila
 It just means that the way I imagine a specification of Rust to look like is as consisting of two parts: The Rust-to-MIR translation, and a specification for MIR.
 If another compiler uses a different implementation strategy, it can still be compliant with the specification; it just has to ensure that Rust programs behave as specified.
 This is a common approach that can also be found, e.g., in the specification of CPU instruction sets: The specification describes the behavior of a complex instruction as a series of commands in some lower-level language.  The CPU does not actually use that language as part of its implementation, but *it behaves as if it would*, and that's the only part that matters.
+**/Update**