(Link)

Authors: Matthieu Sozeau (Inria Nantes), Abhishek Anand (BedRock Systems), Simon Boulier (Inria Nantes), Cyril Cohen (Côte d’Azur University), Yannick Forster (Saarland University), Fabian Kunze (Saarland University), Gregory Malecha (BedRock Systems), Nicolas Tabareau (Inria Nantes), and Théo Winterhalter (Inria Nantes)

Reference: Sozeau, Matthieu, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. “The Metacoq Project.” Journal of Automated Reasoning 64, no. 5 (2020): 947-999.

Why this paper? Cited by Layered Modal Type Theory: Where Meta-programming Meets Intensional Analysis, Trocq: Proof Transfer for Free, With or Without Univalence, and The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant

I’ve written before about Coq, recently renamed to Rocq, a proof assistant based on Martin-Löf’s dependent type theory. This paper, along with various sequels written in the six years since the project was first announced, aims to mechanise the syntax and semantics of Rocq, in Rocq.

Implementing domain specific languages is a classic use case of functional programming, and Rocq is at heart a functional language with an unusually expressive type system and so well suited to the task. Implementing a language in itself might seem more exotic, but it is quite common; Lean is an example of a dependently typed language that is so `bootstrapped’. Rocq is implemented in OCaml rather than itself, and while this paper does not extend to a complete implementation (important features such as the termination checker on recursive code are missing), that is one direction of future work.

Implementing a dependently typed language in itself of course offers one the possibility of formally verifying the implementation. I am not sure, but I do not believe this was done for the Lean implementation. Verifying Rocq using Rocq may naively seem a particularly vicious circularity – if we are genuinely worried that Rocq is flawed, we cannot trust a proof in Rocq that it is not, and if we are convinced it is perfect, the verification adds no confidence. But this is to apply too crude a notion of how proof assistants help us trust our proofs; the aim is to (hopefully radically) increase our confidence in results, not to gain a mythical level of 100% confidence. In particular a hypothetical proof of Rocq’s correctness could be examined by humans to reduce the likelihood that it is being accepted due only to a flaw in Rocq.

A cool thing about this project is that it is structured to provide useful outputs before the full formalisation is completed. To this end the paper features a number of examples of metaprogramming with the tool as developed. This allows users to flick back and forth (‘quote’ and ‘unquote’) between actual Rocq code and the implementation’s internal representation of Rocq syntax, and hence write programs – in some cases verified programs – in Rocq that manipulate Rocq programs via the internal representation. We see examples using the (large) fragment of Rocq already supported of adding a constructor to a type; a certified tactic for proving theorems of intuitionistic propositional logic; a plugin for extending Rocq with new properties without violating consistency; and an extraction from Rocq to the lambda calculus.