When programmers want to prove strong program invariants, they are usually faced with a choice between using theorem provers and using traditional programming languages. The former requires them to provide program proofs, which, for many applications, is considered a heavy burden. The latter provides less guarantees and the programmer usually has to write run-time assertions to compensate for the lack of suitable invariants expressible in the type system. We introduce Mezzo, a programming language in the tradition of ML, in which the usual concept of a type is replaced by a more precise notion of a permission. Programs written in Mezzo usually enjoy stronger guarantees than programs written in pure ML. However, because Mezzo is based on a type system, the reasoning requires no user input. In this paper, we illustrate the key concepts of Mezzo, highlighting the static guarantees our language provides.
@InProceedings{protzenko:OASIcs.FSFMA.2013.68, author = {Protzenko, Jonathan}, title = {{Illustrating the Mezzo programming language}}, booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)}, pages = {68--73}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-56-9}, ISSN = {2190-6807}, year = {2013}, volume = {31}, editor = {Choppy, Christine and Sun, Jun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.68}, URN = {urn:nbn:de:0030-drops-40905}, doi = {10.4230/OASIcs.FSFMA.2013.68}, annote = {Keywords: Type system, Language design, ML, Permissions} }
Feedback for Dagstuhl Publishing