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.