CAREER: Semantic Programming

华盛顿大学：语义编程，Aaron 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.