ATS for Systems Programming with Theorem Proving

Trustees Of Boston University, Boston

Investigators

Abstract

Building software is often a process of great complexity. In this day and age, safe and reliable software is a rare oddity and software failure is a norm rather than an exception. How can safe and reliable software be built in a manner that is practical and cost-effective? This project addresses the issue by focusing on building trustworthy low-level systems that is verifiably safe and reliable. Instead of solely relying on testing to ensure safety and reliability, the novel approach taken in the project provides the programmer with a formal means to construct proofs demonstrating correctness properties of actual implementation that can be verified independently. This is often referred to as combining programming with theorem-proving. ATS is a programming language equipped with a highly expressive type system rooted in the framework Applied Type System. In particular, both dependent types and linear types are available in ATS. The development of ATS has now reached a point where advanced types can be effectively employed to support the construction of safe and efficient code. Continuing this progress naturally directs us to investigate how the paradigm of combining programming with theorem-proving as is advocated in ATS can be exploited to raise code quality in low-level systems programming. The project is expected to yield significant contributions to the understanding of type theory and its application to the design and implementation of low-level systems. In particular, advanced type theory (involving dependent types and linear types) is to be developed to facilitate the use of types in capturing programming invariants.