SHF: Small: Effectful Software Contracts

点击翻译按钮获取中文摘要

The long-term goals of this project are to bring the technology ofsoftware contracts to widely-used programming languages and, throughthe use of manifest contracts, to provide software developers with amigration path from simply typed code to fully functional correctness.Since computational effects are notoriously hard to reason about andpervade even the simplest realistic programs, the proposed researchshould have significant impact on programmers' ability to developsoftware that is more reliable and more secure. Contracts in software establish clear interfaces between programcomponents. Like contracts in the legal realm, they delineate eachparty's expectations and obligations. Such contracts are becomingincreasingly 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 formalsemantics and must be supported by a monitoring system that preciselytracks the flow of values as they cross interfaces. To date, however,the formal study of contracts has mostly been limited to smallidealized languages without computational effects, such as readingdata from or writing data to a display or file, managing resourcessuch as memory, and performing probabilistic or speculativecomputation.This research aims to extend the semantic framework of softwarecontracts to languages with various computational effects: theextension is qualitative in nature and will enable the use ofcontracts in new application domains. Specifically, the PIs proposeto add support for computational effects to the two flavors ofcontracts studied to date: latent contracts, which are runtime checksnot reflected in the type system, and manifest contracts, where asystem of precise types records the most recent runtime check appliedto each value. The extension of latent contracts will be done in thecontext of a monadic met language. The extension of manifestcontracts will make use of a variant of Hoare Type Theory to preciselyrecord computational effects. The PIs will also implement prototypesystems and use them to present novel applications of softwarecontracts.