Discussing "The Coq Proof Assistant"

(Link)

Authors: The Coq Development Team

Reference: The Coq Development Team. The Coq proof assistant, Version 8.16, September 5 2022

Why this reference? Cited by Type Theory as a Language Workbench and Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

This blog is a project to encourage myself to read more widely, and hopefully spread some knowledge to those who stumble across it, by looking at multiple-cited papers in my recent Google Scholar recommendations. Yet papers are not the only thing that gets cited; I’ve looked at books, monumental pairs of books, and now, my first software. Reviewing software in a week is not an obvious task, as the ‘content’ of software is not encapsulated by looking at source code, but also lives beyond the software in the ecosystem around it – tutorials, libraries, applications, active forums and communities, and so forth. In order to make this task tractable, I’ve decided to concentrate on the Coq User Manual as my reference, and use that to give an overview of Coq.

At its base, Coq is an implementation of a certain version of Martin-Löf Type theory. The intention as usual is to provide a type system expressive enough to naturally express mathematical statements, along with tools to allow users to attempt to prove these statements in an interactive style, with the computer checking each step and assisting with automatic proving where possible. Coq has enjoyed conspicuous success in this, with the manual making particular mention of the CompCert verified C compiler and verification of the four colour theorem.

The name, which is French for rooster but inevitably attracts sniggers, is a play on CoC, the Calculus of Constructions, the version of type theory the original software was based on in 1983. It also works as a pun on the name of Thierry Coquand, whose PhD thesis provided the original impetus (the original software was mostly written by Gérard Huet). The version of type theory that is currently the basis of Coq is CIC, the Calculus of Inductive Constructions, as introduced by Coquand and Christine Paulin-Mohring. This does not mean that the underlying type theory is fixed and static however; for example there was major development on the treatment of coinduction between versions 8.5 and 8.9 (2015-18), and there are currently two elements of the trusted base that are labelled as experimental (universe polymorphism and a type of proof-irrelevant propositions).

The first layer built on top of the implementation of the core language CIC are the language extensions, which are translated to the core language in a process called elaboration. To give some idea of relative sizes, the manual spends 97 pages on the core language, and 120 on the extensions. Features such as implicit coercions and typeclasses allow the user to write more natural looking mathematical statements with less clutter, wherever said clutter can be inferred automatically.

The ability to express mathematical statements is not particularly valuable without the ability to prove them. Naively, one might expect proofs to proceed in a functional style, as CIC is essentially a functional language with a particularly expressive type system. Indeed, every Coq proof is ‘really’ a functional program, which can be inspected. But in practice these programs are not written directly in functional style but rather generated in imperative style by commands called tactics, which are called in sequence and modify the state of a proof (its current goals and assumptions). Some tactics are fairly low level, for example moving the left hand side of an implication goal into the assumptions. Others are considerably more sophisticated, attempting to automatically discover non-trivial proofs in a style reminiscent of the logic programming language Prolog. There is also a bifurcation between two major packages of tactics, the standard collection and an independently produced collection SSReflect; these are intended to be merged in the future. Note that neither of these collections of tactics, nor any others, need to be trusted: they attempt to produce proofs, but these ‘proofs’ are not accepted until the core language type-checks them successfully.

If the default tactics are not sufficient, users can create their own using a language called Ltac. This language is described by the manual as somewhat ad hoc and unclear in its semantics, and so another currently experimental feature (good enough that users are encouraged to try it) is Ltac2, a tactic-definition language enhanced with desirable programming language features such as types.

As one would expect for a mature language, there have been a range of libraries and plugins developed for Coq. Again, even the most basic libraries do not need to be trusted, as they can be checked by the core type checker. There are also several choices of IDEs, a range of introductory books and tutorials, and so on. One style of plugin that is of particular note is the ability to extract code from Coq to other programming languages (currently Haskell, Scheme, and OCaml). At best, this creates certified-correct code that can run in a more efficient system than Coq. At worst, code extraction is not completely reliable due to mismatches between the semantics of Coq and the target languages, and so the manual even features a brief section colourfully titled “Extraction’s horror museum”.