Home » forums » LtU Forum

The Mezzo programming language

I saw a link to the Mezzo programming language on Hacker News, and I came here to see what had already been discussed. To my surprise there seems to be hardly a mention about it. So I figured I'd post and perhaps stir up a discussion.

According to the Mezzo website the language has been formalized in Coq and is:

... a programming language in the ML tradition, which places strong emphasis on the control of aliasing and access to mutable memory. A balance between simplicity and expressiveness is achieved by marrying a static discipline of permissions and a dynamic mechanism of adoption and abandon.

By hellertime at 2014-05-06 03:37 | LtU Forum | previous forum topic | next forum topic | other blogs | 6441 reads

Comment viewing options

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

Separation logic and language design

One way to present Mezzo would be to describe it as the first attempt to design a ML language on top of separation logic. Of course, that's a bit reductive: Mezzo's type system is inspired by separation logic rather than a direct translation of it, and ML influences makes it nicer than the program logics we usually see, intended for C-family languages. At the same time I'm always surprised that this had not been done before -- despite the copious amount of research that is done on concurrent separation logics these days.

By gasche at Thu, 2014-05-08 13:18 | login or register to post comments