CAREER: Compilers for Dependable Computational Mathematics

计算数学中使用的算法越来越复杂，现代文明在从设计到设备控制的各个层面都严重依赖于科学软件。 然而，用于将算法表达为计算机程序的编程语言和工具并没有以匹配的速度发展，在可证明正确的已验证算法和它们的代码实现之间留下了不断扩大的差距。 软件系统中的故障可能会造成人员伤亡，每年造成数十亿美元的损失。 此外，模拟软件的无声故障会严重破坏科学模型的可信度，带来深刻的知识责任。 这个研究项目将调查基于形式方法的原则和工具，使编程实践成为普通程序员更数学化的活动。其首要目标是使可靠性成为关键软件的一个基本属性。为此，PI将设计一个新的编程系统，支持基于新的逻辑语言结构的公理编程研究，发明基于形式推理和方法的新编程模型和工具。 PI将研究数学软件的实用依赖类型系统的设计及其有效编译，以支持集成的自动推理和计算机代数系统。 该项目具有协同组件，在符号和代数计算、编译器构造、证明理论和教育之间架起了桥梁。 从这个项目中获得的见解将被整合到新的课程中，并由一本关于现代类型系统和编译器的实际实现的书来支持。 PI期望发现公理化编程的基本原理、工具和技术。 这些结果有望影响现有主流编程语言（如C++）在支持结构化泛型编程和提高软件可靠性方面的发展。 与以往一样，PI将涉及本科生和研究生两个层次的学生，在动手，完全整合的研究为基础的课程。

Algorithms used in computational mathematics are increasinglysophisticated and complex; and the modern civilization criticallydependents on scientific software at all levels from design toequipment control. Yet, the programming languages and tools used toexpress algorithms as computer programs do not progress at a matchingpace, leaving an expanding gap between provably correct publishedalgorithms and their realizations in code. Failures in softwaresystems can cost human lives and are responsible for billions ofdollars lost annually. Furthermore, silent failures of simulationsoftware can seriously undermine the credibility of a scientificmodel, entailing profound intellectual liabilities. This researchproject will investigate formal-methods-based principles and tools tomake the practice of programming a more mathematical activity forordinary programmers. The overriding aim is to make dependability acommon basic property of critical software. To that end, the PI will design a new programming system that supportsresearch in axiomatic programming based on new logical linguisticconstructs, invent new programming models and tools grounded in formalreasoning and methods. The PI will investigate the design of practicaldependent type systems for mathematics software and their efficientcompilation to support integrated automated deduction and computeralgebra systems. The project has synergistic components that buildbridges between symbolic and algebraic computation, compiler construction,proof theory, and education. Insights gained from this project willbe integrated into new courses, supported by a book on the practicalimplementation of modern type systems and compilers. The PI expectsto discover basic principles of axiomatic programming, tools, andtechniques. The results are expected to influence the evolution ofexisting major mainstream programming languages (such as C++) intheir support for structured generic programming and improvement of software reliability. As ever, the PI will involve students both atthe undergraduate and graduate levels, in hands-on, fully integratedresearch-based classes.