In a previous post, I talked about a proposed approach to drafting the unsafe code guidelines. Specifically, I want to the approach of having an executable specification of Rust with additional checks that will signal when undefined behavior has occurred. In this post, I want to try to dive into that idea a bit more and give some more specifics of the approach I have in mind. I’m going to focus on this post on the matter of the proper use of shared references &T – I’ll completely ignore &mut T for now, since those are much more complicated (because they require a notion of uniqueness).

While I was at POPL the last few days, I was reminded of an idea regarding how to bring more struture to the unsafe code guidelines process that I’ve been kicking around lately, but which I have yet to write about publicly. The idea is fresh on my mind because while at POPL I realized that there is an interesting opportunity to leverage the “blame” calculation techniques from gradual typing research. But before I get to blame, let me back up and give some context.

I spent a really interesting day last week at Northeastern University. First, I saw a fun talk by Philip Haller covering LaCasa, which is a set of extensions to Scala that enable it to track ownership. Many of the techniques reminded me very much of Rust (e.g., the use of “spores”, which are closures that can limit the types of things they close over); if I have time, I’ll try to write up a more detailed comparison in some later post.

I’ve been thinking about the unsafe code guidelines a lot in the back of my mind. In particular, I’ve been trying to think through what it means to “trust types” – if you recall from the Tootsie Pop Model (TPM) blog post, one of the key examples that I was wrestling with was the RefCell-Ref example. I want to revisit a variation on that example now, but from a different angle. (This by the way is one of those “Niko thinks out loud” blog posts, not one of those “Niko writes up a proposal” blog posts.)

A little while back, I wrote up a tentative proposal I called the “Tootsie Pop” model for unsafe code. It’s safe to say that this model was not universally popular. =) There was quite a long and fruitful discussion on discuss. I wanted to write a quick post summarizing my main take-away from that discussion and to talk a bit about the plans to push the unsafe discussion forward.

The importance of the unchecked-get use case

For me, the most important lesson was the importance of the “unchecked get” use case. Here the idea is that you have some (safe) code which is indexing into a vector:

In my previous post, I spent some time talking about the idea of unsafe abstractions. At the end of the post, I mentioned that Rust does not really have any kind of official guidelines for what kind of code is legal in an unsafe block and what is not.What this means in practice is that people wind up writing what “seems reasonable” and checking it against what the compiler does today. This is of course a risky proposition since it means that if we start doing more optimization in the compiler, we may well wind up breaking unsafe code (the code would still compile; it would just not execute like it used to).