Home

Type soundness and race freedom for Mezzo

Type soundness and freedom for Mezzo,
Thibaut Balabonski, François Pottier, and Jonathan Protzenko,
2014

Full paper
Presentation slides

The programming language Mezzo is equipped with a rich type system that controls aliasing and access to mutable memory. We incorporate shared-memory concurrency into Mezzo and present a modular formalization of its core type system, in the form of a concurrent λ-calculus, which we extend with references and locks. We prove that well-typed programs do not go wrong and are data-race free. Our definitions and proofs are machine-checked.

The Mezzo programming language has been mentioned recently on LtU. The article above is however not so much about the practice of Mezzo or justification of its design choices (for this, see Programming with Permissions in Mezzo, François Pottier and Jonathan Protzenko, 2013), but a presentation of its soundness proof.

I think this paper is complementary to more practice-oriented ones, and remarkable for at least two reasons:

  • It is remarkably simple, for a complete soundness proof (and race-freeness) of a programming language with higher-order functions, mutable states, strong update, linear types, and dynamic borrowing. This is one more confirmation of the simplifying effect of mechanized theorem proving.
  • It is the first soundness proof of a programming language that is strongly inspired by Separation Logic. (Concurrent) Separation Logic has been a revolution in the field of programming logics, but it had until now not be part of a full-fledged language design, and this example is bound to be followed by many others. I expect the structure of this proof to be reused many times in the future.
By gasche at 2014-05-18 09:53 | Type Theory | other blogs | 23175 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Videos of the talk

François Pottier recently gave two lectures on Mezzo at Institut Henri Poincaré.
They were recorded and the videos just got posted on Youtube: part one and part two.

By adrieng at Mon, 2014-05-19 21:48 | login or register to post comments

A few lessons from the Mezzo project

We were discussing the difficulties inherent to discussing design inside the academic programming-languages community. In this light I found the Mezzo submission to the new SNAPL conference fairly interesting.

A few lessons from the Mezzo project
François Pottier and Jonathan Protzenko
2015

With Mezzo, we set out to design a new, better programming language. In this modest document, we recount our adventure: what worked, and what did not; the decisions that appear in hindsight to have been good, and the design mistakes that cost us; the things that we are happy with in the end, and the frustrating aspects we wish we had handled better.

I tried to find a few choice quotes that would be representative of parts that could support my point (besides "there is a full page about the some of the choices of syntax" and "there are a lot of examples"), but I think the index of the paper is actually more instructive:

# A word about Mezzo

# Some fundamental design decisions

# Growing the language
## Syntax, syntax, syntax
## Algebraic datatypes are central
## Ownership is central
## Flexible ownership via adoption and abandon
## Beyond duplicable versus affine?

# Looking at some code
## Example 1: One-shot functions (using existentials)
## Example 2: Futures (using strong update)
## Example 3: Mutable balanced trees (using value-dependent types)
## Example 4: Containers of non-duplicables (using borrowing)

# Difficulties revealed by the implementation
## The state of the implementation

# The proof of Mezzo (soundnes and data-race freedom)

# What now?

By gasche at Thu, 2015-05-07 13:14 | login or register to post comments