ATS for Systems Programming with Theorem Proving

构建软件通常是一个非常复杂的过程。在这个时代，安全可靠的软件是罕见的怪事，软件故障是一种常态，而不是例外。如何才能以实用和经济高效的方式构建安全可靠的软件？该项目将重点放在构建可验证的安全可靠的可信赖的低级系统上，从而解决这个问题。该项目所采用的新方法不再仅仅依靠测试来确保安全性和可靠性，而是为程序员提供了一种形式化的方法来构造证明，以证明实际实现的正确性性质，并且可以独立验证。这通常被称为编程和定理证明的结合。ATS是一种编程语言，它配备了一个高度表达的类型系统，植根于框架应用类型系统。特别是，ATS中既有从属类型，也有线性类型。ATS的开发现在已经到了可以有效地使用高级类型来支持安全高效的代码构造的地步。继续这一进程自然会引导我们研究如何利用ATS中倡导的编程与定理证明相结合的范例来提高低级系统编程中的代码质量。预计该项目将对理解类型理论及其在低级别系统的设计和实施中的应用作出重大贡献。特别是，高级类型理论(涉及依赖类型和线性类型)将被开发，以促进在捕获编程不变量时使用类型。

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.