Programatica: The Early Years — A Personal Recollection

Presented as part of the 2001 HCSS conference.

Abstract

Current program development environments provide excellent support for many desirable aspects of modern software applications such as performance and interoperability, but almost no support for features that could directly enhance correctness and reliability. In this talk, I will describe the first steps that we are making in a project to develop a new kind of program development environment. Our goal is to produce a tool that actively supports and encourages its users in thinking about, stating, and validating key properties of software as an integral part of the programming process.

The environment that we are designing, called Programatica, will allow programmers to assert properties of program elements as part of their source code, capturing intuitions and insights about its behavior at the time it is written. These property assertions will also provide an opportunity to give more precise interfaces to software components and libraries. Even by themselves, assertions can provide valuable documentation, and can be type checked to ensure a base level of consistency with executable portions of the program. Critically, however, our environment will allow property assertions to be annotated with "certificates" that provide evidence of validity. By adopting a generic interface, many different forms of certificate will be supported, offering a wide range of validation options -- from low-cost instrumentation and automated testing, to machine-assisted proof and formal methods. Individual properties and certificates may pass through several points on this spectrum as development progresses, and as higher levels of assurance are required. To complete the environment, a suite of "property management" tools will provide users with facilities to browse or report on the status of properties and associated certificates within a program, and to explore different validation strategies.

We plan to evaluate our system by applying it to some real-world, security related problems, and we hope to demonstrate that it can contribute to the development of more robust and dependable software applications. For example, a tighter integration between programming and validation should provide the mechanisms that we need to move towards a model for accountability in software, and away from the ubiquitous "as is" warranties that we see today. More specifically, this could allow vendors to provide and sell software on the strength of firm guarantees about its behavior, and allow users to identify the responsible parties when a software system fails.