Algorithms used in computational mathematics are increasingly sophisticated and complex; and the modern civilization critically dependents on scientific software at all levels from design to equipment control. Yet, the programming languages and tools used to express algorithms as computer programs do not progress at a matching pace, leaving an expanding gap between provably correct published algorithms and their realizations in code. Failures in software systems can cost human lives and are responsible for billions of dollars lost annually. Furthermore, silent failures of simulation software can seriously undermine the credibility of a scientific model, entailing profound intellectual liabilities. This research project will investigate formal-methods-based principles and tools to make the practice of programming a more mathematical activity for ordinary programmers. The overriding aim is to make dependability a common basic property of critical software.
To that end, the PI will design a new programming system that supports research in axiomatic programming based on new logical linguistic constructs, invent new programming models and tools grounded in formal reasoning and methods. The PI will investigate the design of practical dependent type systems for mathematics software and their efficient compilation to support integrated automated deduction and computer algebra systems. The project has synergistic components that build bridges between symbolic and algebraic computation, compiler construction, proof theory, and education. Insights gained from this project will be integrated into new courses, supported by a book on the practical implementation of modern type systems and compilers. The PI expects to discover basic principles of axiomatic programming, tools, and techniques. The results are expected to influence the evolution of existing major mainstream programming languages (such as C++) in their support for structured generic programming and improvement of software reliability. As ever, the PI will involve students both at the undergraduate and graduate levels, in hands-on, fully integrated research-based classes.
