What exactly happens when you panic!()? I recently spent a lot of time looking at the parts of the standard library concerned with this, and it turns out the answer is quite complicated! I ...

I have blogged a few times before about Stacked Borrows, my proposed aliasing model for Rust. But I am a researcher, and what researchers (are expected to) do is write papers—so that’s what...

My advisor Derek and some of my coauthors Amin, Robbert and Lars just put out a blog post on the SIGPLAN blog on the idea of “semantic typing”. This is the methodology behind RustBelt, so t...

This post is about uninitialized memory, but also about the semantics of highly optimized “low-level” languages in general. I will try to convince you that reasoning by “what the hardware d...

Less than a month ago, I announced Stacked Borrows 2. In particular, I hoped that that version would bring us closer to proper support for two-phase borrows. Turns out I was a bit too optim...

When formalizing a proof in an interactive theorem prover like Coq, one reoccurring issue is the handling of algebraic hierarchies. Such hierarchies are everywhere: some operations are ass...

Recently, I have significantly updated Stacked Borrows in order to fix some issues with the handling of shared references that were uncovered in the previous version. In this post, I will d...

Running your unsafe code test suite in Miri has just gotten even easier: Miri is now available as a rustup component! Huge thanks to @oli-obk and @mati865 who made this happen. Miri can ru...

Sometimes, I run software that I trust less. All software I use on a daily basis is open-source, but there is still closed-source software I run occasionally, like video games. Unfortunatel...

Last week, I was in Berlin at the Rust All-Hands 2019. It was great! I will miss nerding out in discussions about type theory and having every question answered by just going to the person ...

It is that time of the year again where our feedreaders are filled with people’s visions for what Rust should become in the next year. Coming up with a vision is not exactly my strong suit,...

My internship (“research assistantship”) with Mozilla has ended several weeks ago, and this post is a report of the most recent tweaks I made to Miri and Stacked Borrows. Neither project is...

I am currently applying for academic positions, and several people recommended I get a Google Scholar profile because hiring committees will look for that. I even found one vacancy that exp...

Three months ago, I proposed Stacked Borrows as a model for defining what kinds of aliasing are allowed in Rust, and the idea of a validity invariant that has to be maintained by all code a...

When talking about the Rust type system in the context of unsafe code, the discussion often revolves around invariants: Properties that must always hold, because the language generally assu...

In this post, I am proposing “Stacked Borrows”: A set of rules defining which kinds of aliasing are allowed in Rust. This is intended to answer the question which pointer may be used when t...

This summer, I am again working on Rust full-time, and again I will work (amongst other things) on a “memory model” for Rust/MIR. However, before I can talk about the ideas I have for this ...

For some time now (since the 1.26 release, to be precise), Rust has a very powerful machinery for CTFE, or compile-time function evaluation. Since then, there have been various discussions ...

While I was busy doing Rust-unrelated research, RustBelt continues to move and recently found another bug (after a missing impl !Sync that we found previously): It turns out that Arc::get_m...

After my internship last year has ended, I naturally became somewhat less active in the Rust community as I could not work on Rust full-time any more. Well, for the following months I am go...

Last week, I blogged about my efforts to fight mailman subscription spam. Enabling SUBSCRIBE_FORM_SECRET as described there indeed helped to drastically reduce the amount of subscription s...

I recently noticed that both of the Mailman setups that I am running are being abused for subscription spam: Bots would automatically attempt to subscribe foreign email addresses to public ...

I finally have a setup that I am happy with for syncing contacts between my phone and my laptop. Most would probably consider that a solved problem, but I have an extra requirement that rul...

In my last post, I talked about the new “pinned references” which guarantee that the data at the memory it points to will not, ever, be moved elsewhere. I explained how they enable giving a...

Recently, a new API for “pinned references” has landed as a new unstable feature in the standard library. The purpose of these references is to express that the data at the memory it points...

This post is about an aspect of the RustBelt paper. Concretely, I’d like to share some of our thoughts on the nature of types and shared references. Let’s see how well this goes. :) Shared...

Last week, I was in Los Angeles at POPL 2018 to present our paper RustBelt: Securing the Foundations of the Rust Programming Language. The talk has been recorded, so if you want to get a 20...

I think all HTTP communication on the internet should be encrypted – and thanks to Let’s Encrypt, we are now much closer to this goal than we were two years ago. However, when I set up Let...

POPL 2018, the conference where I will present our RustBelt paper, is doing a series of interviews with senior and junior people from the community: People of Programming Languages. They al...

Yesterday was the last day of my Rust internship at Mozilla. I can hardly believe that twelve weeks have passed since that post, but my calendar insists. If you want to see what I have done...

Some weeks ago, I described Types as Contracts as an approach for how to go about defining Rust’s aliasing-related undefined behavior. One key property of this approach is that it is execut...

Over the last couple of weeks of my internship, I have been working on a proposal for the “Unsafe Code Guidelines”. I got some very encouraging feedback at the Mozilla All-Hands, and now I’...

Last year, the Rust unsafe code guidelines strike team was founded, and I am on it. :-) So, finally, just one year later, this post is my take at what the purpose of that team is.

Just yesterday, we submitted our paper RustBelt: Securing the Foundations of the Rust Programming Language. Quoting from the abstract: Rust is a new systems programming language that pr...

A couple of weeks ago, our ongoing effort to formalize Rust’s type system lead to us actually discovering a bug in the Rust standard library: MutexGuard implemented Sync in cases where it s...

It’s now been two weeks since my internship started (two weeks already, can you believe it?). In other words, if I want to post “weekly or bi-weekly” updates, I better write one today ;) . ...

This summer, I am given the awesome opportunity of spending three months in the Mozilla offices in Portland, working on Rust. I am extremely grateful that Mozilla is providing this opportun...

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 o...

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...

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 ...

Do you know the feeling of having done something, and having a website for it somewhere, but not finding the right spot to put a link to that website? I certainly do, and, well… now that I ...

I’ll use this blog to write random articles on things that matter to me, and that I want to share. So far, I don’t know what this will end up being about - probably mostly about programming...