SHF: Small: A Programming Language Ecosystem for Higher-Order Software Contracts

Northwestern University, Evanston IL

Investigators

Abstract

Software contracts promise developers a light-weight mechanism for validating that software conforms to its specifications. Contracts are written in the programming language that developers already use. Thus, developers should be able to use contracts to express with ease expected properties of the inputs and outputs of program components, while the programming language can translate the properties into checks and enforce them as the program runs in real-world conditions. In other words, contracts promise to act as a programmable monitoring system, up-to-date documentation, a driver for testing, and a source of useful debugging information when the behavior of a component goes awry. Unfortunately, developers --- especially those that use modern, so called higher-order, languages such as Python or JavaScript --- do not buy into the promise of contract systems despite four decades of research. Contracts simply are second class citizens in current language ecosystems. The goal of this project is to investigate the design, theory, implementation and practice of a contract-centric programming ecosystem. The project’s novelty is that the mechanisms that higher-order programming languages use to check contracts can be extended to produce information about how the components of a program work together. As a result, this information can be the basis for (i) tools that help developers visualize, debug, and zoom in on the interactions of components; (ii) a system that assists developers with adding contracts to existing code bases. The project's results will impact: (i) developers: the ecosystem will directly facilitate key aspects of their day-to-day work; (ii) language designers and implementers: the project will provide tangible guidelines and evidence for how to improve their languages; and (iii) educators: the project will provide means for demonstrating and teaching the value of specifications in software development. In technical terms, the project's ecosystem will consist of two parts: (i) a contract inference engine for higher-order languages, and (ii) tools for contract-centered debugging, visual inspection, and simplification of code. Each part will benefit the other. The tools will suggest where to add contracts, and inferred contracts will improve the effectiveness of the tools. The ecosystem's design will yield a novel proxy mechanism for higher-order languages that reflects on the structure and evaluation of a program to expose information about how its components interact. The project’s evaluation of the ecosystem will build on the extensive work of the user community of Racket --- an academic language that is also used in industry --- on collecting benchmark suites with interesting contracts. The investigator and his group will develop a prototype of the ecosystem together with mathematical models that communicate its salient features. The purpose of the prototype is to demonstrate the feasibility and usefulness of the ecosystem. The purpose of the mathematical models is to provide a blueprint for language designers and implementers. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.