SHF: SMALL: Language-agnostic Proofs

编程语言的正确性对于开发可靠的软件至关重要。因此，语言设计者经常努力从数学上证明他们的编程语言满足键的正确性。这些证明通常遵循一种模式，这种模式不仅适用于一种语言，而且适用于大量其他语言。该项目的新颖之处在于(i)发现发展语言不可知论证明所必需的科学知识，即适用于语言类而不是一种语言的证明，以及（ii）提供证据证明语言不可知论证明是验证编程语言的有效工具。该项目的影响是(i)为快速验证编程语言提供合适的方法和软件工具，从而导致更正确和可靠的软件，以及（ii）以普遍化和可教的形式描述编程语言证明方法的核心见解。该项目开发了一种用于表达语言无关证明的领域特定语言，并实现了一个软件工具，该工具可以根据编程语言定义和作为输入的语言无关证明自动生成机器检查的证明。该项目还开发了与语言无关的证明，这些证明捕获了大多数常见状态语言的类型安全，并演示了使用这些证明来自动生成许多编程语言的类型安全的机械化证明，包括WebAssembly和Middleweight Java等语言。正如预期的那样，某些具有复杂特性的语言的类型安全性不能通过本项目提供的与语言无关的证明来建立。尽管如此，这些证明使一种基于其有用的部分输出的方法成为可能，也就是说，它们可以为大量复杂语言生成机械化证明，然后可以将其用作手动完成证明的开端。该项目从具有复杂特性的编程语言文献中演示了这种方法，并记录了该方法的有效性。这个项目提供的与语言无关的证明类似于为应用于许多语言而编写的伪代码。因此，这些证明可以用广义的观点来教授类型安全，研究者正在将它们包含在编程语言的课程中。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.