Gagallium

In the previous blog post, I introduced a new framework for reasoning about programs: permissions, a sort of hybrid between a type system and a program logic. The main selling point is that it allows one to reason in a finer-grained manner about programs. The current incarnation of the permission mechanism is Mezzo, a language in the tradition of ML.

The first question that comes fairly naturally is: why are we going such great lengths trying to design such a complex reasoning framework? Here are some answers:

• since mutable portions of the heap have a unique owner, programs written in Mezzo enjoy the property that they are data-race free, that is, we may never have two people trying to access a writable location at the same time;
• thus, we are allowed to perform strong updates, that is, updates that change the type of a variable.

The latter item may seem of dubious usefulness; indeed, the mswap example that I used seems artificial, and I have never needed it in practice. However, the example of concat at the end of the previous post is much more useful: it is emblematic of a more general concept of “destination-passing-style” algorithms that allow one to write functions in a safe, tail-recursive way, without resorting to unsafe hacks.

However, as I hinted in the conclusion of the previous blog post, with the elements I have presented so far, there are some serious limitations.

In this blog post, I will introduce a novel mechanism called adoption and abandon, which allows one to safely alias mutable data, while remaining inside the permission framework; in particular, this means we’ll continue to guarantee the unique-owner property for mutable blocks. Of course, there’s no free lunch: this adoption and abandon mechanism incurs a dynamic cost at runtime.

Some of you may have heard about it already: this blog post is about a new programming language that’s being designed right there at Gallium, codenamed Mezzo.

Designing a new programming language is nothing out of the extraordinary: many students in our research area do it for a living, and I’m no exception. I’ve been doing the traveling salesman, running presentations of Mezzo all over the place: Texas, New York, and going even as far as Plateau de Saclay. Now is the time for a blog post.

Mezzo is a joint work between François Pottier, my advisor, and myself. Recently, Thibaut Balabonski joined our team as a post-doctoral researcher to work on the concurrent aspects of the language; we also had an undergrad intern, Henri Chataing, work on the compilation part of the project.

Mezzo draws inspiration from many other research projects; I don’t want to bother the reader with a long introduction – this is not a research paper: I will provide an extended comparison of our work with other material in a later blog post. For the moment, let me just mention that we blend ideas from affine type systems, separation logic, and systems based on regions and capabilities.

Mezzo is still in a preliminary stage, but I feel like it is time to start the revolution, and introduce this almighty language to a wider audience. Behold!