SHF: SMALL: Language-agnostic Proofs

The correctness of programming languages is paramount for the development of reliable software. Accordingly, language designers often engage in an effort to mathematically prove that their programming languages satisfy key correctness properties. These proofs often follow a schema that does not apply just to one language but, rather, applies to a plethora of other languages. The project’s novelties are (i) to discover the scientific knowledge necessary for developing language-agnostic proofs, that is, proofs that apply to classes of languages rather than to one language, and (ii) to provide evidence that language-agnostic proofs are an effective tool for validating programming languages. The project's impacts are (i) to provide suitable methods and a software tool for quickly validating programming languages, which leads to more correct and reliable software, and (ii) to delineate the core insights of proof methods for programming languages in a generalized and teachable form. This project develops a domain-specific language for expressing language-agnostic proofs and implements a software tool that automatically produces machine-checked proofs from a programming language definition and a language-agnostic proof given as input. This project also develops the language-agnostic proofs that capture the type safety of most common stateful languages and demonstrates the use of these proofs to automatically generate the mechanized proof of type safety of a number of programming languages, including languages such as WebAssembly and Middleweight Java. As expected, the type safety of some languages with sophisticated features cannot be established with the language-agnostic proofs that this project offers. Nonetheless, these proofs enable an approach based on their useful partial outputs, that is, they can generate a mechanized proof for a large fragment of sophisticated languages, which then can be used as a head start to manually complete the proof. The project demonstrates this approach on programming languages from the literature with sophisticated features and documents the effectiveness of the approach. The language-agnostic proofs that this project offers are akin to pseudocode that is written to apply to many languages. Therefore, these proofs can be used for teaching type safety with a generalized perspective, and the investigator is including them within a course in programming languages. 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.