CAREER: Semantic Programming

摘要0448275 Aaron D. Stump 华盛顿大学职业：语义编程，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.