add two recently submitted papers

[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 1b7269be7e2902b7322278a1b24a5214e350d9e9..c8a7252ec018c3c7bd6d1ff27bbc4336b2a1ff3e 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
+title: "Day 1 of My Mozilla Internship, or: How to Specify Program Behavior?"
 categories: internship rust
 ---
 
@@ -36,3 +36,18 @@ What exactly do the guarantees "mutable borrows don't have aliases" and "the poi
 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.
+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!
+We *have* a complete and non-ambiguous definition of how Rust code is to be translated to MIR code.
+(Currently, this definition exists only in code; ideally, one day, it will also exist in natural language as part of a specification document.)
+As a second advantage, MIR is *much* simpler than Rust: It has way fewer operations, no syntactic sugar, less redundancy.
+(In fact, that's the entire reason why MIR was introduced into the compiler.)
+Specifying the behavior of a MIR program can concentrate on the parts that really matter, without focusing on details like how exactly a `for`-loop desugars into lower-level operations.
+
+Now, this is *not* to say that every Rust compiler has to use MIR in its compilation pipeline.
+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.