From: Ralf Jung Date: Wed, 7 Jun 2017 01:24:54 +0000 (-0700) Subject: Capitalize Things X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/a7be6d6b7e841ec4ea671fc38fb5902e7b7cfbea Capitalize Things --- diff --git a/personal/_posts/2015-10-12-formalizing-rust.md b/personal/_posts/2015-10-12-formalizing-rust.md index 9f5dc7a..b867ffb 100644 --- a/personal/_posts/2015-10-12-formalizing-rust.md +++ b/personal/_posts/2015-10-12-formalizing-rust.md @@ -37,13 +37,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. -## 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. -## 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. @@ -54,7 +54,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. -## 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. @@ -76,7 +76,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! -## 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: diff --git a/personal/_posts/2017-05-23-internship-starting.md b/personal/_posts/2017-05-23-internship-starting.md index 1b7269b..54361c2 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: Day 1 of My Mozilla Internship categories: internship rust ---