X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/a7be6d6b7e841ec4ea671fc38fb5902e7b7cfbea..2099972f4110e06db8b6452d4511b991efb896c7:/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 54361c2..149b4f3 100644 --- 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: "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. +**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. ;) @@ -36,3 +38,19 @@ 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. +**/Update**