SHF: SMALL: Language-agnostic Proofs

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

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.