Programming with Effects in Coq
Next-generation programming languages will move beyond simple type systems to include support for formal specifications and mechanically- checked proofs of adherence to those requirements. Already, in the imperative world, languages such as ESC/Java and Spec# integrate Hoare- style pre- and post-conditions into the underlying type system. However, we argue that neither the program logics used in these systems, nor the decision procedures used to discharge verification conditions, are sufficient for establishing deep properties of modular software.
In contrast, the Coq proof development environment provides a powerful program logic (CiC) coupled with an extensible, interactive environment that can combine deep insights from humans with automation to discharge deep proof obligations. Unfortunately, the language at the core of Coq is limited to purely functional programming.
In the Ynot project, we are attempting to address this problem by extending Coq with a new type constructor (the Hoare-triple type), and a few carefully chosen axioms that can be used to build imperative programs in a style quite close to Haskell. I will report on our progress thus far, both in using Ynot to construct modular, extensible libraries for imperative programs, as well as our new compiler infrastructure for generating efficient code from Ynot programs.