A Case Study in Dependent Type Theory: Extracting a Certified Program from the Formal Proof of its Specification

Abstract

Proofs are an important part of mathematics, but they are not without their flaws. Most proofs are written by humans, and humans make mistakes. In this thesis, we explore the use of proof assistants to construct formal versions of informal proofs, and to extract certified and correct programs from these formal proofs. We study a specific case of two problems from lattice theory, solved by Bezem and Coquand in [2]. Firstly, we ask ourselves: are the results from [2] correct? The informal proofs posed in [2], used to justify the correctness of the results, are complex enough that mistakes are possible. Using the Coq proof assistant, we formalize parts of the proofs from [2], to gain more confidence in the correctness of these informal proofs. Secondly, is the process of formalization a feasible one? Transforming an informal proof into a formal proof is not necessarily an easy or straightforward process, and there are several approaches to formalization of a proof. Lastly, is the process of formalization worth the effort? A fully formalized proof gives us almost complete confidence in the correctness of the proof, and hence the result. Moreover, if the proof is constructive, we get the added bonus of extracting a certified program from the proof. In our case, this program has some practical use cases in a real-world setting, mostly as a prototype. Our formalization, done using Coq, can be found in the GitHub repository at [1]. For convenience, the formal proof of the central result has been reproduced in Listing A.1.