Homotopy Type Theory: Programming and Verification

软件故障的代价确实令人震惊。众所周知的个人案例包括火星气候轨道器故障(8000万GB)、阿丽亚娜火箭灾难(3.5亿GB)、奔腾芯片部门故障(3亿GB)，以及最近的心脏出血错误(EST。GB 4亿)。还有很多更多的例子。更糟糕的是，爱国者导弹系统的一次故障和Therac-25辐射系统的一次故障已经夺去了生命。更广泛地说，美国政府2008年的一项研究估计，有缺陷的软件每年给美国经济造成1000亿GB的损失。有许多成功的软件验证方法(测试、模型检查等)。一种方法是找到保证软件正确性的数学证明。然而，现代软件的复杂性意味着手写的数学证明可能是不可信的，这导致了对软件正确性的计算机检查证明的需求日益增长。Coq、AGDA、NuPRL和IDRIS等程序设计语言和交互证明系统都是基于一个称为Martin-Löf类型理论的形式系统开发的。在这些系统中，我们不仅可以编写程序，还可以用类型来表示程序的性质，并编写程序来表示我们的程序是正确的。这样，无论是像四色定理这样的大型数学定理，还是像CompCert C编译器这样的大型软件系统，都得到了形式上的验证。然而，在这样的大型项目中，出现了可伸缩性的问题：我们如何使用这些系统来有效地构建经过验证的大型软件库？这与可重用性和模块化问题有关：软件系统中的一个组件应该可以由另一个组件替换，该组件的行为相同，即使它可能以完全不同的方式构建。也就是说，我们需要一个在计算上表现良好的“扩展相等”(也就是说，我们希望使用这个相等来运行程序)。实现这种平等是一个根本性的难题，40多年来一直没有得到解决，但现在看来我们可能有了解决的办法！菲尔兹勋章获得者弗拉基米尔·沃沃茨基对这个问题提出了完全不同的看法，他认为等式是数学中最抽象的分支之一，即同伦理论中出现的路径，导致了同伦类型理论(Hott)。在Hott中，如果两个对象的行为相同，则它们完全可以互换。然而，Hott的大多数陈述都涉及缺乏计算合理性的公理，因此，我们没有基于Hott的编程语言或验证系统。我们项目的目标是解决这一问题，从而开发出第一个基于Hott的新型编程语言和验证系统，并开发向程序员和那些对正式验证感兴趣的人展示Hott的力量的案例研究。我们是进行这项研究的理想团队，因为i)我们拥有从Hott的基础到编程语言和验证工具的实现和部署的独特技能和想法；以及ii)该领域最重要的人物(包括Voevodsky)以及行业参与的积极合作，以确保我们牢记我们的最终目标-可用的编程语言和验证工具。

The cost of software failure is truly staggering. Well known individual cases include the Mars Climate Orbiter failure (£80 million), Ariane Rocket disaster (£350 million), Pentium Chip Division failure (£300 million), and more recently the heartbleed bug (est. £400 million). There are many, many more examples. Even worse, failures such as one in the Patriot Missile System and another in the Therac-25 radiation system have cost lives. More generally, a 2008 study by the US government estimated that faultysoftware costs the US economy £100 billionannually. There are many successful approaches to software verification(testing, model checking etc). One approach is to find mathematicalproofs that guarantees of software correctness. However, thecomplexity of modern software means that hand-written mathematicalproofs can be untrustworthy and this has led to a growing desire forcomputer-checked proofs of software correctness. Programming languages and interactive proof systems like Coq, Agda,NuPRL and Idris have been developed based on a formal system calledMartin-Löf Type Theory. In these systems, we can not only writeprograms, but we can also express properties of programs using types,and write programs to express proofs that our programs are correct.In this way, both large mathematical theorems such as the Four ColourTheorem, and large software systems such as the CompCert C compilerhave been formally verified. However, in such large projects, theissue of scalability arises: how can we use these systems to build largelibraries of verified software in an effective way?This is related to the problem of reusability and modularity: acomponent in a software system should be replaceable by another whichbehaves the same way even though it may be constructed in a completelydifferent way. That is, we need an "extensional equality" which iscomputationally well behaved (that is, we want to run programs usingthis equality). Finding such an equality is a fundamental anddifficult problem which has remained unresolved for over 40 years.But now it looks like we might have a solution! Fields medallistVladimir Voevodsky has come up with a completely different take on theproblem by thinking of equalities as paths such as those which occurin one of the most abstract branches of mathematics, namely homotopytheory, leading to Homotopy Type Theory (HoTT). In HoTT, two objectsare completely interchangeable if they behave the same way. However,most presentations of HoTT involve axioms which lack computationaljustification and, as a result, we do not have programming languagesor verification systems based upon HoTT. The goal of our project isto fix that, thereby develop the first of a new breed of HoTT-basedprogramming languages and verification systems, and develop casestudies which demonstrate the power of HoTT to programmers andthose interested in formal verification.We are an ideal team to undertake this research because i) we haveunique skills and ideas ranging from the foundations of HoTT to theimplementation and deployment of programming language and verificationtools; and ii) the active collaboration of the most important figuresin the area (including Voevodsky) as well as industrial participationto ensure that we keep in mind our ultimate goal -- usable programminglanguage and verification tools.