open some things in new tabs

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

diff --git a/personal/_posts/2015-10-12-formalizing-rust.md b/personal/_posts/2015-10-12-formalizing-rust.md
index 9f5dc7ae39225a5ee81ee0ac1be4c0e60275de83..548fbd9297a6dc9b67814ad768c454d905a27166 100644 (file)
--- a/personal/_posts/2015-10-12-formalizing-rust.md
+++ b/personal/_posts/2015-10-12-formalizing-rust.md
@@ -15,7 +15,9 @@ 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.
 This goes hand-in-hand with other approaches like testing, fuzzing and [static analysis](https://homes.cs.washington.edu/~emina/pubs/crust.ase15.pdf).
 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.
 This goes hand-in-hand with other approaches like testing, fuzzing and [static analysis](https://homes.cs.washington.edu/~emina/pubs/crust.ase15.pdf).

-However, we (at my [research group](http://plv.mpi-sws.org/)) are into formalizing things, so that's what we are going to do.
+However, we (at my [research group](http://plv.mpi-sws.org/)) are into formalizing things, so that's what we are going to do as part of the [RustBelt](http://plv.mpi-sws.org/rustbelt/) research project.
+
+**Update:** Added link to RustBelt website.

 
 <!-- MORE -->
 
 
 <!-- MORE -->
 


@@ -37,13 +39,13 @@ The first version is also not going to cover automatic destructors, i.e., the `D
 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.
 
 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?
+## So What's Left?

 
 You may wonder now, what are we even doing then?
 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.
 
 
 You may wonder now, what are we even doing then?
 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
+## 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.
 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.
 
 We could now be looking at the checks the Rust compiler is doing, and prove directly that these checks imply memory safety.
 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.


@@ -54,7 +56,7 @@ In the following, we will consider programs containing `unsafe` as not being wel
 (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.
 
 (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.
 

-## Semantics to the rescue
+## Semantics to the Rescue

 
 Intuitively, why do we even think that a program that uses `Vec`, but contains no `unsafe` block *itself*, should be safe?
 It's not just the compiler checks making sure that, e.g., we don't call `push` on a shared borrow.
 
 Intuitively, why do we even think that a program that uses `Vec`, but contains no `unsafe` block *itself*, should be safe?
 It's not just the compiler checks making sure that, e.g., we don't call `push` on a shared borrow.


@@ -76,7 +78,7 @@ This is in contrast to the *syntactic* notion of well-typedness of a function, w
 Only recently, research has been able to scale up such semantic methods to languages that combine state (i.e., mutable variables, a heap) with higher-order functions -- languages like Rust, where I can take a closure (a `Fn{,Mut,Once}`) and store it in memory, for later use.
 Lucky enough, my advisor [Derek Dreyer](http://www.mpi-sws.org/~dreyer/) is one of the world experts in this field, which permits me to intensively study Rust (which I would have done anyways) and call it research!
 
 Only recently, research has been able to scale up such semantic methods to languages that combine state (i.e., mutable variables, a heap) with higher-order functions -- languages like Rust, where I can take a closure (a `Fn{,Mut,Once}`) and store it in memory, for later use.
 Lucky enough, my advisor [Derek Dreyer](http://www.mpi-sws.org/~dreyer/) is one of the world experts in this field, which permits me to intensively study Rust (which I would have done anyways) and call it research!
 

-## What we are doing
+## What We Are Doing

 
 So, that's what we are trying to do: Come up not only with a formal version of Rust's (syntactic) type system, but also with appropriate *semantics* for these types.
 We then have to show that the syntactic types make semantic sense. This recovers, in a very roundabout way, the result I mentioned above:
 
 So, that's what we are trying to do: Come up not only with a formal version of Rust's (syntactic) type system, but also with appropriate *semantics* for these types.
 We then have to show that the syntactic types make semantic sense. This recovers, in a very roundabout way, the result I mentioned above: