From 336966b6e6435f3f7722ffd789f822a6d636312b Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 13 Oct 2015 13:01:47 +0200 Subject: [PATCH] Rust post: tune wording --- personal/_posts/2015-10-12-formalizing-rust.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/personal/_posts/2015-10-12-formalizing-rust.md b/personal/_posts/2015-10-12-formalizing-rust.md index f78d418..30bb24a 100644 --- a/personal/_posts/2015-10-12-formalizing-rust.md +++ b/personal/_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? -- 2.30.2