Homotopy Type Theory: Programming and Verification

软件故障的代价确实是惊人的。众所周知的个别案例包括火星气候轨道器失败（8000万英镑），阿丽亚娜火箭灾难（3.5亿英镑），奔腾芯片部门失败（3亿英镑），以及最近的心脏出血错误（4亿英镑）。还有很多很多的例子。更糟糕的是，诸如爱国者导弹系统和Therac-25辐射系统的故障造成了生命损失。更广泛地说，美国政府2008年的一项研究估计，有缺陷的软件每年给美国经济造成1000亿英镑的损失。有许多成功的软件验证方法（测试、模型检查等）。一种方法是找到保证软件正确性的数学证明。然而，现代软件的复杂性意味着手写的数学证明可能是不可信的，这导致了对计算机检查软件正确性证明的日益增长的需求。编程语言和交互式证明系统，如Coq、Agda、NuPRL和Idris，都是基于形式系统calledMartin-Löf类型理论开发的。在这些系统中，我们不仅可以编写程序，还可以使用类型表示程序的属性，并编写程序来表示我们的程序是正确的证明。通过这种方式，大型数学定理（如四色定理）和大型软件系统（如CompCert C编译器）都得到了正式验证。然而，在这样的大型项目中，可伸缩性的问题出现了：我们如何使用这些系统以有效的方式构建经过验证的软件的大型库？这与可重用性和模块化问题有关：软件系统中的一个组件应该被另一个以相同方式运行的组件所替代，即使它可能以完全不同的方式构建。也就是说，我们需要一个在计算上表现良好的“扩展等式”（也就是说，我们希望使用这个等式来运行程序）。找到这种平等是一个基本而困难的问题，40多年来一直没有解决。但现在看起来我们可能有解决方案了！菲尔兹奖得主弗拉基米尔·沃沃斯基（vladimir Voevodsky）提出了一个完全不同的方法来解决这个问题，他将等式视为路径，就像那些发生在数学中最抽象的分支之一，即同伦理论中的路径一样，从而导致同伦类型理论（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.