The long-term goals of this project are to bring the technology of software contracts to widely-used programming languages and, through the use of manifest contracts, to provide software developers with a migration path from simply typed code to fully functional correctness. Since computational effects are notoriously hard to reason about and pervade even the simplest realistic programs, the proposed research should have significant impact on programmers' ability to develop software that is more reliable and more secure.
Contracts in software establish clear interfaces between program components. Like contracts in the legal realm, they delineate each party's expectations and obligations. Such contracts are becoming increasingly important for the regulation of modern software systems, providing an expressive framework for verification and error tracking. To be effective in a software environment, contracts must have formal semantics and must be supported by a monitoring system that precisely tracks the flow of values as they cross interfaces. To date, however, the formal study of contracts has mostly been limited to small idealized languages without computational effects, such as reading data from or writing data to a display or file, managing resources such as memory, and performing probabilistic or speculative computation.
This research aims to extend the semantic framework of software contracts to languages with various computational effects: the extension is qualitative in nature and will enable the use of contracts in new application domains. Specifically, the PIs propose to add support for computational effects to the two flavors of contracts studied to date: latent contracts, which are runtime checks not reflected in the type system, and manifest contracts, where a system of precise types records the most recent runtime check applied to each value. The extension of latent contracts will be done in the context of a monadic met language. The extension of manifest contracts will make use of a variant of Hoare Type Theory to precisely record computational effects. The PIs will also implement prototype systems and use them to present novel applications of software contracts.
