CAREER: Semantic Programming

abstract: 0448275 Aaron D. Stump华盛顿大学正确的软件从来没有像现在这样具有社会重要性，然而开发正确软件的方法仍然过于昂贵，无法广泛使用。该项目旨在对编程范式进行根本性的改变，以合理的成本创建可证明正确的代码。该项目建议开发新的编程语言，在这些语言中，程序可以用紧密集成的形式正确性证明来编写。证明是编程语言中的数据，就像布尔值或字符串一样。类型检查确保如果函数需要证明某些事实（例如，指针不为空）才能正确操作，则在调用函数时确实提供了这样的证明。函数也可以产生证明作为其输出的一部分。必须解决的技术问题出现在支持在可变状态（即，其值可以改变的程序变量）和其他影响的存在下进行编程的证明。拟议工作的更广泛影响包括开发用于正确编程的新语言，以及公开可用的原型实现；以及为研究生和高级本科生开设新课程，融入研究的理念。该提案还包括K-12外展部分。

ABSTRACT0448275 Aaron D. StumpWashington UniversityCAREER: 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 studentsand advanced undergraduates incorporating the ideas of the research. The proposal also includes a K-12 outreach component.