Homotopy Type Theory: Programming and Verification

点击翻译按钮获取中文摘要

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.