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.
With (partial) support from this grant, we were able to design and implement ATS/Postiats (that is, ATS2), which can be seen as a complete overhaul of ATS/Anairiats (that is, ATS1). We were also able to evaluate ATS2 in the context of building a real-time operating system (RTOS). The design and implementation of ATS2 officially started in March, 2011, and it took about 2 years and 6 months for the first version of ATS2 to be ready for public release. As of now, there have already been more than a dozen official releases of ATS2 made to the public. The current released version of ATS2 is nearly entirely written in ATS1, consisting of more than 150K lines of code for its compiler portion and more than 50K lines of code for its library portion. The advanced template system in ATS2 makes it possible to effectively apply functional style of programing to implementing low-level systems while requiring no support of run-time garbage collection (GC). Under the supervision of the PI (Hongwei Xi), Matthew Danish implemented in ATS1 several modules of the Terrier RTOS, including its scheduler and memory management system. He then ported these modules to ATS2. In addition, he made the primary effort in writing/publishing/presenting various papers about applying advanced type theory to implementing low-level systems. Also, there are strong interests in ATS among people outside Boston University. For instance, the following two cases generated some very good publicity for ATS: ATS2 was used by a third party (Chris Double) to provide a fix for the infamous Heartbleed security bug. ATS2 was planned to be used by a third party (Kiwamu Okabe) in the Metasepi project for a re-implementation of NetBSD. The PI (Hongwei Xi) has been using ATS2 as the primary programming language in teaching several CS courses (CS320, CS511 and CS520) at Boston University, allowing both graduate and undergraduate students to learn the state-of-art of program verification in the context of practical programming. There are many forms of support for learning/using ATS on-line. Here is the official website for the ATS programming language: http://ats-lang.org/ There is also an active forum for the users of ATS: https://groups.google.com/forum/?fromgroups#!forum/ats-lang-users