This week, I have been at the Paris Rust Meetup. Meeting all sorts of Rust people was great fun, and the Mozilla offices in Paris are absolutely impressive. You should totally check them out if you have a chance.
On that meetup, I gave a short talk about the current status of my formalization of the Rust type system.
I’d like to talk about an important aspect of dealing with unsafe code, that still regularly seems to catch people on the wrong foot:
When checking unsafe code, it is not enough to just check the contents of every
The “scope” in the title refers to the extent of the code that has to be manually checked for correctness, once
unsafe is used.
What I am saying is that the scope of
unsafe is larger than the
unsafe block itself.
It turns out that the underlying reason for this observation is also a nice illustration for the concept of semantic types that comes up in my work on formalizing Rust (or rather, its type system). Finally, this discussion will once again lead us to realize that we rely on our type systems to provide much more than just type safety.
Update (Jan 11th): Clarified the role of privacy; argued why
evil is the problem.
My current research project – and the main topic of my PhD thesis – is about developing a semantic model of the Rust programming language 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 and written 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, 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 have been found 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. However, we (at my research group) are into formalizing things, so that’s what we are going to do.