0448275 Aaron D. Stump Washington University
CAREER: Semantic Programming, Aaron Stump.
Correct software has never been more societally important, yet approaches to developing correct software remain too costly for widespread use. This project aims to make a fundamental alteration to the programming paradigm, to enable the creation of provably correct code at a reasonable cost. The project proposes to develop new programming languages where programs can be written with tightly integrated formal proofs of correctness. Proofs are data in the programming language, just like booleans or strings. Type checking ensures that if a function requires a proof of some fact (e.g., a pointer is not null) in order to operate correctly, such a proof is indeed supplied where the function is called. Functions may also produce proofs as part of their output. Technical problems that must be solved arise in supporting programming with proofs in the presence of mutable state (i.e., program variables whose values can change) and other effects. Broader impacts of the proposed work include developing new languages for correct programming, together with publicly available prototype implementations; and the creation of new courses for graduate students and advanced undergraduates incorporating the ideas of the research. The proposal also includes a K-12 outreach component.
