publish UB blog post

[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 3ad7cfa0a82faf050abd8726d757749fb0e45e93..43a1a710099c870734febcaa33256a3016aec64f 100644 (file)
--- a/personal/_posts/2015-10-12-formalizing-rust.md
+++ b/personal/_posts/2015-10-12-formalizing-rust.md
@@ -1,20 +1,23 @@
 ---
 title: Formalizing Rust
 categories: research rust
 ---
 title: Formalizing Rust
 categories: research rust

+reddit: /rust/comments/3ofkz6/formalizing_rust/

 ---
 
 ---
 

-My current research project - and the main topic of my PhD thesis - is about developing a *semantic model* of the [Rust programming language](https://www.rust-lang.org/) and, most importantly, its type system.
+My current research project -- and the main topic of my PhD thesis -- is about developing a *semantic model* of the [Rust programming language](https://www.rust-lang.org/) and, most importantly, its type system.

 Rust is an attempt of Mozilla to find a sweet spot in the design space of programming languages: A language that provides low-level resource management (making it a systems language), is convenient for programmers and guards against memory errors and thread unsafety.
 Rust is an attempt of Mozilla to find a sweet spot in the design space of programming languages: A language that provides low-level resource management (making it a systems language), is convenient for programmers and guards against memory errors and thread unsafety.

-Other have [said](https://www.youtube.com/watch?v=O5vzLKg7y-k) and [written](http://www.oreilly.com/programming/free/files/why-rust.pdf) a lot on why we need such a language, so I won't lose any more words on this.
+Other have [said](https://www.youtube.com/watch?v=O5vzLKg7y-k) and [written](https://www.oreilly.com/programming/free/files/why-rust.pdf) a lot on why we need such a language, so I won't lose any more words on this.

 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 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.
 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 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.
+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).
 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](https://plv.mpi-sws.org/)) are into formalizing things, so that's what we are going to do as part of the [RustBelt](https://plv.mpi-sws.org/rustbelt/) research project.
+
+**Update:** Added link to RustBelt website.

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


@@ -24,7 +27,7 @@ Let me just get this out of the way at the beginning: The formal model is not go
 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.
 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.
+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.
 
 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.
 


@@ -36,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.


@@ -51,14 +54,14 @@ However, such a proof only gets us so far: The moment your program uses [`unsafe
 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.)
 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.
+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.

-We also rely on `Vec` *behaving well* - or, I should rather say, *behaving well-typed*.
-Yes, `Vec` uses `unsafe` - but it should not be possible to *observe* this in a well-typed safe program, calling only the interface provided by `Vec`.
+We also rely on `Vec` *behaving well* -- or, I should rather say, *behaving well-typed*.
+Yes, `Vec` uses `unsafe` -- but it should not be possible to *observe* this in a well-typed safe program, calling only the interface provided by `Vec`.

 There are some rules that Rust enforces, some invariants that safe, well-typed code automatically upholds, that people writing unsafe code have to maintain themselves.
 `Vec` performs checks and bookkeeping to get its tracking of the size and capacity of the container right.
 `RefCell` counts the number of outstanding borrows, to make sure at run-time that no two mutable borrows to the same cell exist.
 There are some rules that Rust enforces, some invariants that safe, well-typed code automatically upholds, that people writing unsafe code have to maintain themselves.
 `Vec` performs checks and bookkeeping to get its tracking of the size and capacity of the container right.
 `RefCell` counts the number of outstanding borrows, to make sure at run-time that no two mutable borrows to the same cell exist.


@@ -72,10 +75,10 @@ The core idea is that we can define the inhabitants of a type solely in terms of
 For example, to check that a function is semantically well-typed, you check what it does on every well-typed input, and make sure the output makes sense.
 It doesn't matter *how* the function performs these operations.
 This is in contrast to the *syntactic* notion of well-typedness of a function, which involves looking at the *code* of the function and checking it against a bunch of rules.
 For example, to check that a function is semantically well-typed, you check what it does on every well-typed input, and make sure the output makes sense.
 It doesn't matter *how* the function performs these operations.
 This is in contrast to the *syntactic* notion of well-typedness of a function, which involves looking at the *code* of the function and checking it against a bunch of rules.

-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](https://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:


@@ -87,7 +90,7 @@ In this case, we have to go back to step one and change the semantics of our typ
 By combining this manual proof with the first result covering all syntactically well-typed Rust programs, we finally obtain the desired proof that safe programs using only the unsafe bits that were proven correct, are memory safe.
 No matter what the safe client does with the exposed API of the unsafe data structures, we then know in a mathematical rigorous way that everything will be all right.
 Isn't this a beautiful theorem? I certainly think so, even with the [caveats](#scope) described above.
 By combining this manual proof with the first result covering all syntactically well-typed Rust programs, we finally obtain the desired proof that safe programs using only the unsafe bits that were proven correct, are memory safe.
 No matter what the safe client does with the exposed API of the unsafe data structures, we then know in a mathematical rigorous way that everything will be all right.
 Isn't this a beautiful theorem? I certainly think so, even with the [caveats](#scope) described above.

-We've only recently started this though, there is still a long way to go - lots of fun to be had.
+We've only recently started this though, there is still a long way to go -- lots of fun to be had.

 I will track my progress, in very high-level terms, in [this Rust issue](https://github.com/rust-lang/rust/issues/9883).
 
 Once we got a proper semantic model, we also hope to be able to translate some of these insights back into the vocabulary of Rust programmers, and tell them what it is they have to be checking when writing unsafe Rust code.
 I will track my progress, in very high-level terms, in [this Rust issue](https://github.com/rust-lang/rust/issues/9883).
 
 Once we got a proper semantic model, we also hope to be able to translate some of these insights back into the vocabulary of Rust programmers, and tell them what it is they have to be checking when writing unsafe Rust code.