While the essential ideas of program verification have been understood for decades, the practical ability to develop and maintain correct software at a reasonable cost has remained elusive. Approaches based on manually proving extracted verification conditions are often viewed as brittle and burdensome, despite continued advances. Mostly automatic techniques like static analysis and model checking face challenges scaling to rich properties of large systems. Yet, as societies become increasingly dependent on software systems, the need for a practical way to build provably correct software has never been greater.
Recent work is exploring alternative, language-based approaches to program verification. In these approaches, the programming language provides mechanisms which allow the programmer to express, in some way, her knowledge of why her code meets its specification. This knowledge is connected more intimately to the code than is usually the case for theorem proving approaches. One commonly used mechanism is dependent types. Specifications are expressed as types, and the programming language allows proofs of those specifications to be expressed as terms inhabiting those types. Pre- and post-conditions of functions are recorded in their input and return types, and the functions require and produce proofs of those conditions as additional inputs and outputs. One exciting possibility is that languages for programming with proofs may enable developers to target a "continuum of correctness," through varying amounts of effort on specification and verification.
The proceedings of the
workshop will most likely be archived using ENTCS or as a technical
report (online) at one of the organizers' institutions.