From: Ralf Jung Date: Tue, 13 Oct 2015 11:01:47 +0000 (+0200) Subject: Rust post: tune wording X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/fc0e15c2f39dcef23bbf3ab4e9fea0b61892a727?hp=860f317515838546fab7f5f47b154192f3b52d9d Rust post: tune wording --- diff --git a/ralf/_posts/2015-10-12-formalizing-rust.md b/ralf/_posts/2015-10-12-formalizing-rust.md index f78d418..30bb24a 100644 --- a/ralf/_posts/2015-10-12-formalizing-rust.md +++ b/ralf/_posts/2015-10-12-formalizing-rust.md @@ -3,8 +3,8 @@ title: Formalizing Rust categories: research rust --- -My current research project - and the main topic of my PhD thesis - is about developing a *formal model* of the [Rust programming language](https://www.rust-lang.org/) and 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 control (making it a systems language), is convenient for programmers and guards against memory errors and thread unsafety. +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. 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. 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. @@ -34,7 +34,9 @@ I have some good ideas for how to handle them later, should we have the time for 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. -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. +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. ## So what's left?