split CSS into several files; take some CSS from the default jekyll skeleton

[web.git] / ralf / _posts / 2015-10-12-formalizing-rust.md

diff --git a/ralf/_posts/2015-10-12-formalizing-rust.md b/ralf/_posts/2015-10-12-formalizing-rust.md
index 30bb24a561565d2f7d899860b25499bfa9031d28..3ad7cfa0a82faf050abd8726d757749fb0e45e93 100644 (file)
--- a/ralf/_posts/2015-10-12-formalizing-rust.md
+++ b/ralf/_posts/2015-10-12-formalizing-rust.md
@@ -9,7 +9,7 @@ Other have [said](https://www.youtube.com/watch?v=O5vzLKg7y-k) and [written](htt
 Let me just use this opportunity for a shameless plug: If you are curious and want to learn Rust, check out [Rust-101](https://www.ralfj.de/projects/rust-101/main.html), a hands-on Rust tutorial I wrote.
 I am going to assume some basic familiarity with Rust in the following.
 
 Let me just use this opportunity for a shameless plug: If you are curious and want to learn Rust, check out [Rust-101](https://www.ralfj.de/projects/rust-101/main.html), a hands-on Rust tutorial I wrote.
 I am going to assume some basic familiarity with Rust in the following.
 

-Why do we want to formalize Rust? First of all, I'm (becoming) a programming languages researcher, and Rust is an interesting new language to study.
+Why do we want to do research on Rust? First of all, I'm (becoming) a programming languages researcher, and Rust is an interesting new language to study.

 It's going to be fun! Honestly, that's enough of a reason for me.
 But there are other reasons: It shouldn't be a surprise that [bugs](https://github.com/rust-lang/rust/issues/24292) have [been](https://github.com/rust-lang/rust/issues/25860) [found](https://github.com/rust-lang/rust/issues/24880) in Rust.
 There are lots of things that can be done about such bugs - my take on this is that we should try to *prove*, in a mathematical rigorous way, that no such bugs exist in Rust.
 It's going to be fun! Honestly, that's enough of a reason for me.
 But there are other reasons: It shouldn't be a surprise that [bugs](https://github.com/rust-lang/rust/issues/24292) have [been](https://github.com/rust-lang/rust/issues/25860) [found](https://github.com/rust-lang/rust/issues/24880) in Rust.
 There are lots of things that can be done about such bugs - my take on this is that we should try to *prove*, in a mathematical rigorous way, that no such bugs exist in Rust.


@@ -20,38 +20,35 @@ However, we (at my [research group](http://plv.mpi-sws.org/)) are into formalizi
 
 ## Scope
 
 
 ## Scope
 

-Let me just get this out of the way at the beginning: The first formal model is not going to cover all features of Rust.
-Some of the missing pieces will hopefully be added later, some maybe not.
-Rust is huge, it's too large to be all handled in a single go.
-In particular, the first version is not going to cover automatic destructors, i.e., the `Drop` trait and the dropck mechanism.
-This is, of course, a significant gap, even more so since dropck may well be the most subtle part of the type system, and the current version (as of Rust 1.3) is [known to be unsound](https://github.com/rust-lang/rust/issues/26656).
-But we have to start somewhere, and even without `Drop`, there is a lot to be done.
+Let me just get this out of the way at the beginning: The formal model is not going to cover all features of Rust.
+Some of the missing pieces will hopefully be added later, some maybe not, and some just don't matter for what I am attempting to do.
+Our focus is on the type system, on ownership and borrowing and the ideas these concepts found on.
+Many features of Rust are pretty much orthogonal to this, so I won't attempt to model them accurately.
+This starts with the language itself: The syntax, the concrete set of primitive operations (except for those that concern pointers), the structure of code with modules and crates - none of this really matters.
+I have some idea what to do with traits, unwinding and a few other pieces, but trying to get all of that right in the beginning would just be a distraction.
+In terms of what we are interested in, these features do not significantly change the game.

 
 

-We are also not going to have traits, unwinding and a few other pieces in the beginning.
-This is mostly to avoid getting distracted by all the details, and keep the focus on the most important bits.
-In terms of what we are interested in, none of these features significantly change the game.
-I have some good ideas for how to handle them later, should we have the time for that.
+With Rust introducing the [MIR](https://github.com/rust-lang/rfcs/blob/master/text/1211-mir.md), the compiler actually moved much closer to the kind of minimalist language we are using as a model of Rust.
+So, there's some hope we might eventually establish a formal connection between rustc and our work through MIR.
+But for now, that is out of scope.

 
 

-Finally, our language and type system are not going to be exactly Rust, but something that's more amenable for formal verification.
-Of course, we have to be careful not to introduce any significant differences on this level.
-But the truth is, the actual details of the language are not all that interesting for what we are studying.
-The most important bit is the borrow checker, and the ideas it founds on - not how exactly some corner of the language behaves.
-Still, with Rust introducing the [MIR](https://github.com/rust-lang/rfcs/blob/master/text/1211-mir.md), the compiler actually moved much closer to our "rust-y" language.
-So, there's some hope we might eventually establish a formal connection between MIR and our work.
+The first version is also not going to cover automatic destructors, i.e., the `Drop` trait and the dropck mechanism.
+This is, of course, a significant gap, even more so since dropck may well be the most subtle part of the type system, and the current version (as of Rust 1.3) is [known to be unsound](https://github.com/rust-lang/rust/issues/26656).
+But we have to start somewhere, and even without `Drop`, there is a lot to be done.

 
 ## So what's left?
 
 You may wonder now, what are we even doing then?
 
 ## So what's left?
 
 You may wonder now, what are we even doing then?

-We are focusing on the core type system: Ownership and borrowing.
-The goal is to prove that well-typed Rust programs are *memory and thread safe*, which, roughly speaking, means that all executed pointer accesses are valid, and there are no data races.
+The goal is to prove that programs following Rust's rules of ownership, borrowing and lifetimes are *memory and thread safe*, which, roughly speaking, means that all executed pointer accesses are valid, and there are no data races.

 I will often just say "memory safety", but concurrency is definitely part of the story.
 
 ## The syntactic approach and its limitations
 
 We could now be looking at the checks the Rust compiler is doing, and prove directly that these checks imply memory safety.
 I will often just say "memory safety", but concurrency is definitely part of the story.
 
 ## The syntactic approach and its limitations
 
 We could now be looking at the checks the Rust compiler is doing, and prove directly that these checks imply memory safety.

-This is of course an important property, and actually, this [has been done](ftp://ftp.cs.washington.edu/tr/2015/03/UW-CSE-15-03-02.pdf) already.
-However, such a proof only gets us so far: The moment your program uses [`unsafe`](https://doc.rust-lang.org/stable/book/unsafe.html), this result does not apply to your program any more.
-It is the whole purpose of `unsafe` to permit writing dangerous code that the compiler cannot check, and hence any proof relying solely on such compiler checks simply does not apply.
+Let us call these checks Rust's type system, then we are looking for the classic result of *type soundness*: Well-typed programs don't go wrong.
+This is of course an important property, and actually, it [has been proven](ftp://ftp.cs.washington.edu/tr/2015/03/UW-CSE-15-03-02.pdf) already.
+However, such a proof only gets us so far: The moment your program uses [`unsafe`](https://doc.rust-lang.org/stable/book/unsafe.html), this result does not apply any more.
+It is the whole purpose of `unsafe` to permit writing dangerous code that the compiler cannot check, and hence it cannot be covered by any proof relying solely on such compiler checks.

 In the following, we will consider programs containing `unsafe` as not being well-typed.
 (We could also consider them well-typed in a more liberal type system that above result does not, and cannot, apply to. This is closer to what the Rust compiler does, but it's not helpful in our context.)
 Note that this issue is viral: `Vec`, `RefCell`, `Rc` - all these and many more standard library data structures use `unsafe`, any if your program uses any of them, you're out of luck.
 In the following, we will consider programs containing `unsafe` as not being well-typed.
 (We could also consider them well-typed in a more liberal type system that above result does not, and cannot, apply to. This is closer to what the Rust compiler does, but it's not helpful in our context.)
 Note that this issue is viral: `Vec`, `RefCell`, `Rc` - all these and many more standard library data structures use `unsafe`, any if your program uses any of them, you're out of luck.