The cost-effective construction of functionally correct software systems remains an unmet challenge for Computer Science. Although industrial best practices for software construction (such as testing, code reviews, automatic bug finding) have low cost, they cannot provide strong guarantees about correctness. Classical verification methods, on the other hand, are not cost-effective. Recently, the research community has been exploring the idea of dependent types, which extend the expressive power of programming languages to support verification. These rich types allow the programmer to express non-trivial invariant properties of her data and code as a part of her program. That way, verification is incremental, localized and at source-language level.
This multi-institution collaborative project is for the design and implementation of a programming language with dependent types, called Trellys. Technically, Trellys is call-by-value functional programming language with full-spectrum dependency. Overall, the project combines numerous fragmented research results into a coherent language design, by building a robust open-source implementation. The design draws on diverse solutions to the technical problems that arise from extending traditional programming languages accommodate dependent types: type and effect inference, language interoperability, compilation, and concurrency.
The remarkable growth of computing through all areas of our society depends critically on programming languages. These languages allow computer programmers to direct the actions of computers in areas like flight-control, medicine, finance, energy infrastructure, and many others. Errors in programs designed for such purposes could be very costly, even life-threatening. Unfortunately, traditional programming languages do not provide a way for programmers to guarantee that their programs have no mistakes. The Trellys project is one attempt to solve this problem by providing tools that assure program correctness through proof. Currently, the best way to ensure correctness of software is to test it in example situations. But at best, testing can only cover a tiny fraction of the vast number of different scenarios that could arise when software is used in practice. In contrast, with mathematical proofs, correctness can be ensured for all possible scenarios. The consequences of this design are potentially momentous for programming practice. This collaboration among researchers Tim Sheard (Portland State), Aaron Stump (The University of Iowa), and Stephanie Weirich (The University of Pennsylvania) developed new programming languages that combine the usual features needed for programming, with new language features for proving properties about programs. Just as in mathematics, a proof provides incontrovertible evidence of the truth of some theorem. In the domain of programming, example theorems could be simple statements like "If you reverse the order of elements in a list, and then reverse the result, you get back the original list". They could also be much more complex statements about the behavior of large pieces of software. By providing programmers with a proof language to complement their usual programming language, this project seeks to give programmers the tools they need to guarantee their software works as intended. Creating languages that combine proofs and programs in a seamless whole is a challenging technical endeavor. One of the central issues is ensuring that the proof language is logically sound: it should not be possible to write down a proof in the language for some statement that is not, in fact, true. Proving soundness is a deep subject in mathematical logic, and the researchers working on Trellys have adapted ideas from logic to show the soundness of logics that reason about and are combined with programs. Trellys explored a number of different language designs, based on different trade-offs between the tightness of the connection between proofs and programs, and the technical difficulty of establishing properties like logical soundness. These different designs are formally described in the associated publications, and many have also been implemented, to enable further experimentation with writing programs and proofs in these advanced new languages. While much progress was made in understanding how proofs and programs can be intertwined, more research and more engineering work is needed to create new, industrial-strength languages incorporating proofs and programs, while providing strong guarantees of properties like logical soundness.
