When Proofs Meet Programs: An Extension of Dependent Type Theory with Church’s Thesis
Christine Paulin-Mohring · Communications of the ACM · 2025
What is a mathematical proof?It can be described as a sequence of logical steps and calculations that serve as evidence of the correctness of a statement.The steps must follow rules that are accepted as correct by the community.One might think there is a set of universal rules.However, this is far from being the case.Gödel's incompleteness theorem tells us that no "reasonable" system will allow us to prove everything that is "true."Instead of searching for ever more powerful theories, one can, on the contrary, restrict the rules of the game to extract more information from the proofs.Let's look at an example.If a formula ∃x, P(x) is true in a certain "world," then, by definition, there exists an element t in the model such that the formula P(x) is true for x = t.What happens at the proof level?If we have proven the formula ∃x, P(x), does there exist a "witness" t and a proof of P(t)?This property is characteristic of so-called "constructive" logics but is not satisfied by usual logic.Indeed, mathematicians classically do not distinguish between the property "there exists x such that P" and its negative version: "it is impossible for P to always be false."To illustrate the difference, let's consider a function f on natural numbers.This function reaches a minimum point (otherwise, one could build an infinite decreasing sequence starting from f(0) ).But this proof does not give us any clue on how to actually construct the minimum of any particular function f.Some "natural" logics preserve the "constructive" nature of the existential quantifier and thus guarantee the existence of witnesses associated with existence proofs.These logics have a strong connection with computer science, as the proofs will not only give us a way to designate the witness but also a way to compute it.The representation of proofs by expressions corresponding to functional programs is known as the Curry-Howard correspondence.This is an essential tool for understanding the dynamics of proofs (very useful in automated theorem proving to restrict the search space).It is also the foundation of several proof assistants, in particular, Coq/Rocq, Agda, and Lean.The interactive proof process ultimately produces an explicit term to represent the proof, which is then verified a posteriori by a program acting as an uncompromising reviewer.The same functional framework is used to represent calculations commonly used in mathematical modeling and proofs.The resulting languages form privileged frameworks both for formalizing mathematics and for representing computational objects.They are grouped under the term "type theory" to distinguish them from the "set theory" traditionally claimed as the foundation of mathematics.