Rust post: tune wording

[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 b661db696fc376aec001c823b85bb420087697f3..30bb24a561565d2f7d899860b25499bfa9031d28 100644 (file)
--- 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's safe to use, convenient for programmers, provides low-level control (making it a systems language) 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?