Dr Nicolas Tabareau from IMT Atlantique Bretagne-Pays de la Loire, provides us with further insight about interactive proof assistants, within the wider field of computer science, software and mathematics
Formal software correctness is gaining traction, with a paroxysmal application to lethal issues in medicine and autonomous vehicles. Interactive proof assistants based on type theory have shown their effectiveness to prove the correctness of important pieces of software like a C compiler [Ler09] or a software-to-hardware toolchain [DeepSpec]. However, they suffer from a major limitation: the absence of effects.
Effects and proof assistants: An impossible marriage?
The general acceptance of interactive proof assistants by non-experts suffers from a major limitation, the absence of effects in their type theory. Indeed, some basic programming paradigms – such as exceptions or mutable memory – are absent from the language of type theory, leading to efficiency issues. Dually, some basic logical principles – such as the excluded middle or the axiom of choice – are also absent from the language, leading to expressivity issues. Taking aside the lack of efficiency and expressivity, the absence of effects forces developers to stay in the “all programs and proofs must be fully specified and terminating” paradigm, which prevents quick prototyping and testing before entering the full certification process.
The addition of effects to a logical system is not a new subject and can be traced back to double-negation translations [Gli29], although the modern standpoint can undoubtedly be attributed to Moggi in his seminal paper [Mog93], as used in the F* project [SWS+13]. Since the inception of dependent type theory, several researchers have tried to apply the techniques coming from simply-typed settings to enrich it with new reasoning principles, typically classical logic.
The early attempts led to mixed results, if not outright failures. Most notably, Barthe and Uustalu showed that writing a typed CPS translation preserving dependent elimination was out of reach [BU02], and similarly, Herbelin proved that CIC is inconsistent with computational classical logic [Her05]. Retrospectively, this should not have been that surprising. This incompatibility is the reflection of a very ancient issue: mixing classical logic with the axiom of choice, whose intuitionistic version is a consequence of dependent elimination, is a well-known source of foundational problems [ML06]. While in the literature much emphasis has been put on the particular case of classical logic, we argue that this is an instance of a broader phenomenon.
Let us explain with an example of why it is not possible to simply add effects naively to a complex logical system using new primitives. Consider the statement “the addition on natural numbers is commutative: ∀ n m : N. n + m = m + n”. This lemma is easy to prove using a proof assistant; by induction on natural numbers. However, the addition of natural numbers is not commutative in the presence of effects because the result of a computation depends on the order of evaluation, which is a well-known fact for any C, Java or Python programmer. Indeed, let us see the consequences of this lemma if the integer expressions under consideration may use mutable state. If n and m are actual values, let say 3 and 5, then the lemma tells us that 8 is equal to 8, which is correct. Now, assume that we have access to a mutable reference x whose initial value is 0 and that n is defined as the expression ‘x:=3; !x’ and m is defined as the expression ‘!x + 2’ (where !x is dereferencing the value stored in x, and := is assigned). Then, assuming that the addition of natural numbers starts with evaluating its left argument, n + m evaluates to 3 + 5 and then to 8, whereas m + n evaluates to 2 + 3; and then to 5. So the lemma tells us that 8 = 5, which is wrong and leads to an inconsistency. A direct consequence is that in an effectful proof assistant, the standard induction principle on natural numbers is not valid anymore, at least not in its full generality.
This incompatibility has been investigated recently and evocatively coined the “Fire Triangle” in a new analysis [PT20]: mixing general induction principles, A.K.A. dependent elimination, substitution, and effects leads to inconsistency, as illustrated in Figure 1 (⊥ corresponds to False).
A more conceptual cause of the incompatibility between effects and type theory lies in what is known as the Curry-Howard correspondence, which tells us that proofs and programs are the very same things. Therefore, extending the expressivity of the language from a programming point of view amounts to extending the expressivity of the logic, which can lead to inconsistencies if the extension is not compatible with the rest of the logical system.
Towards effectful proof assistants
Fortunately, we have been able to analyse the cause of inconsistency in the presence of effects and turn this unforeseen difficulty into a blessing, opening the door to the integration of effects in proof assistants based on the Curry-Howard correspondence. This constitutes a brand new field of investigation for proof assistants as mixing effects and proof assistants were notoriously considered impossible. It explains why developers using proof assistants have accepted to work in an entirely pure setting, whereas they were usually much more familiar with programming languages, providing various kinds of effects, resigned for instance not to use native notions of exceptions, mutable memory or non-terminating functions.
The starting point of our new research project is to build a logical system where effects can be added to the programming language without corrupting the logic. These effects will be added gradually in such a way that the power of the logical system and the expressivity of the programming language can be decided at compile time – according to a trade-off between expressivity and complexity of the theory. This will provide a generation of proof assistants with programming language paradigms familiar to engineers, and at the same time, logical systems closer to the logics mathematicians are used to working with.
References
[BU02] CPS Translating Inductive and Coinductive Types. Barthe G. and Uustalu T..2002. In Proceedings of Partial Evaluation and Semantics-based Program Manipulation. ACM, 131–142.
[DeepSpec] The Science of Deep Specification, the DeepSpec project, https://deepspec.org/
[Gli29] Sur Quelques Points de la Logique de M. Brouwer. Glivenko V. Bulletins de la classe des sciences 15 (1929), 183–188.
[Her05] On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic. Herbelin H..2005. In Seventh International Conference, TLCA ’05, Nara, Japan. April 2005, Proceedings (Lecture Notes in Computer Science), Pawel Urzyczyn (Ed.), Vol. 3461. Springer, 209–220.
[Ler09] Formal verification of a realistic compiler. Leroy X..Comm. of the ACM, 52(7):107-115, 2009.
[ML06] 100 years of Zermelo’s axiom of choice: what was the problem with it? Martin-Löf P. The Computer Journal. 49, 3 (2006) 345–350.
[Mog93] Notions of Computation and Monads. Moggi E. Information and Computation 93, 1 (July 1991), 55–92.
[PT20] The Fire Triangle: How to Mix Substitutions, Dependent Elimination and Effects. Pédrot P.-M., Tabareau N..POPL’20, New-Orleans, USA.
[SWS+13] Verifying Higher-order Programs with the Dijkstra Monad. Swamy N., Weinberger J., Schlesinger C., Chen J., Livshits B. PLDI’13.
*Please note: This is a commercial profile
