Contracts: Semantics and Pragmatics

Matthias Felleisen

At the 1999 opening workshop of PPS--Pierre-Louis Curien's new lab at Paris 7--I presented the first talk on higher-order contracts. Since then these logical interface assertions on higher-order objects have become a subject of intense study. In contrast to contracts for first-order values, higher-order contracts pose challenging questions, mostly concerning their semantics and their pragmatics. The former is about such questions as what these contracts mean and when are contracts satisfied; the latter tries to answer the question whether blaming a specific component is justified when a contract is violated. In this talk, I will show how my joint work with Pierre-Louis Curien on observably sequential functions in the mid 1990s informed our search for a semantics of higher-order contracts. The model has pleasing answers to many questions. Even if it ultimately fails to explain all questions in this realm, it has served as a guideline for many contract design questions for the past ten years. To answer the question on pragmatics, we have to turn to the pragmatics developed by Christos Dimoulas.