Proof Assistants in OOP languages

Question

I am new to the subject of proof assistant software, and I am willing to make one later (about some years later) by myself. I have started self-studying HoTT, Logic and Category theory. But through the little search I had, I have found that most (if not all) of the languages that people use for proof assistant programs, are in fact functional. I wonder what the reason behind this choice is and if one can have the same advantages, or necessities using some other languages, perhaps Java, and Kotlin.

Answer 1

There are many competing concerns when it comes to what languages to use to build a proof assistant.

What is a proof assistant?

A modern proof assistant is actually many parts put together. The most integral part is the kernel which (ideally) is a small self-contained bit of code that does the proof-checking. But most proof assistants also have parsers/elaborators which parse the proof assistant language, and tactics which are little pieces of automation. Also, there are actually two proof languages, the low-level proof language (sometimes based on terms) checked by the kernel and the higher-level proof language which is made up of tactics that build low-level proofs on the fly. The tactics need to be written in some language.

It is not uncommon for different parts to be written in different languages. This is true of say Isabelle (ML and Scala) and Lean (C++ and Lean).

I think some would argue the kernel is the main part of a proof assistant and indeed it is the most important, even if it usually is a very small part of the code. Also for proof languages that can export proofs, it is not uncommon to see many external proof checkers pop up in different languages since they are easy to write and are good for double-checking that the proofs are correct.

Use what you know

While there are good reasons to use certain languages, I think there is also flexibility, and within that flexibility, people like to use the languages they know best. This is especially true for toy proof assistants and external proof checkers.

The right tool for the job

Some tasks are easier in some languages. Functional languages are particularly well-suited to a few things involved in theorem proving. As Alex Nelson already said, they make it easy to build parsers and interpreters. If you have a CS degree, you may have taken a class where you use a simple functional language like Scheme to build a Scheme interpreter.

But even more important than the functional part is the strongly typed part. A common approach to building a theorem prover is the LCF approach (where the ML family of languages arose, and which is common for the HOL-family of proof assistants). In that, you have a type Theorem, and you have some constructors for Theorem. You design these type constructors in such a way that they are the only way you can create Theorem, and the constructors correspond to logically sound rules. This approach is also nice because it means you don't have to store proof steps (but has the downside that can't export proofs easily). You just know that if you have an object of type Theorem, then it must be a valid theorem. But this takes a lot of trust that you won't accidentally have a backdoor approach to building a type of Theorem. This type-safety comes with certain languages (usually functional ones) more than others. (Although someone made a Python implementation of the LCF approach, so I guess anything is possible.)

Also, if you have this very type-safe way to construct Theorem, then your tactics can just be arbitrary code in the same language. You can trust your users to write their own tactics without worrying about the consistency of your proof assistant.

Customizability

Since many proof assistants are based around tactics, it is important for users to be able to write their own tactics. The LCF approach above lets one use the same programming language to write tactics. This tactic language is a meta-language (where the ML family of programming languages get their name) for the proof assistant. But even non-LCF proof assistants want users to write customization. Coq has a bunch of custom languages you can use to write tactics besides the main meta-language OCaml. Lean lets you use the Lean language itself to write tactics. Some tactics also call out to external tools like automated theorem provers or neural networks.

Speed

Proof assistants often have to do a lot of steps to check a proof, this is especially true in two situations: if there are tactics involved, or if there is arbitrary computation built into the proof language. The former is true of most proof assistants, with Metamath being a key counterexample. The latter is true of dependent type theory. So while one wants the proof assistant to be correct, one also wants it to be fast so the user has a good experience.

This is why Lean was originally written in C++, and to this day the Lean 4 kernel is still in C++. It is also why Rust is becoming a popular language for writing proof assistants and proof checkers (since it is very fast but also has some of the functional programming safe coding features).

Eat your own dogfood

In software, there is a notion of "eating your own dog food", namely using your own tools. That is why most compilers are written in the same language being compiled. It is also one reason why Lean 4 moved to being written in Lean 4 (except the C++ kernel). While Lean is one of the few theorem provers which is also a full program language, the "eat your own dogfood" ethos can still apply to the other proof assistants. Type theoretic proof assistants like HOL or dependent type theory have a math language that looks a lot like functional programming, and historically many proof assistant users and developers were in the programming language research community where functional languages and language safety are key concerns. So it isn't surprising they choose to use functional languages.

Extreme assurance

Proof assistants are all about checking the correctness of a proof, and can then be used to check the correctness of other software systems. You want a really high bar of assurance that a proof assistant kernel is correctly implemented. Proof assistant kernels are small so they can be easily inspected. They are also often implemented in very safety-oriented languages like functional languages, or if not, then in a very simple and easy-to-follow code. Nonetheless, bugs still pop up, much to the frustration and embarrassment of the developers. HOL Light had two bugs. Coq had a number. Lean 4 (during development) had one. In all cases, these bugs could be used to prove false theorems.

There are two approaches to dealing with these issues. One is to export proofs so that others can write their own external proof checker. Metamath has a large number of proof checkers. Lean 4 currently has three I think (and these are run during continuous integration of Lean's Mathlib library).

Another approach is to formally verify the code for the kernel. There are a few methods for this, which depend on the language being used to implement the kernel. In HOL-Light, after fixing the bugs, John Harrison formally verified a model of his kernel. Since HOL-Light's math language is close to OCaml, the model was pretty faithful to the actual code. CakeML takes this further by designing a new version of ML which is formally verified in HOL4. Then HOL4 can be run in CakeML. (I don't remember if they verified the HOL4 kernel too.) Metamath Zero (MM0)'s tiny verifier is written in plain C and compiled to very simple x86 bytecode. The plan is to use MM0 (with Peano arithmetic) to verify the bytecode for the MM0 verifier. Moreover, MM0 can act as an external verifier for almost any proof assistant. While Lean 4's main kernel is in C++, Lean4Lean is an external checker written in Lean 4. This may one day become the main Lean kernel if it can become fast enough. Since it is written in pure Lean 4, the plan is to formally verify both that the Lean kernel implements Lean's type theory and that Lean's type theory is consistent (or more formally, equiconsistent with ZFC plus countably many large cardinals or something like that).

Answer 2

The historic reason why most proof assistants are implemented in functional languages is that ML (predecessor to Standard ML and OCaml) was invented to implemented the LCF proof assistant which evolved into the HOL family of proof assistants.

INRIA, the French computer science institute, implemented OCaml and it became their lingua franca (if you'll pardon the pun). It's no surprise that Coq (developed at INRIA) uses OCaml.

I mean, in some sense, it's not surprising: statically typed functional programming languages are designed to make implementing interpreters (and related things) quick and easy.

But some important proof assistants do not use functional languages, for example:

• Automath is implemented in C (originally it was in Pascal)
• Mizar is implemented in Delphi (or Object Pascal) and Mizar in Rust implements certain components in Rust
• Lean4 is implemented in C++

Answer 3

Here are three that are implemented in non-functional languages:

• Arend is implemented in Java.
• Lean 3 is implemented in C++.
• Metamath has verifiers implemented in C, Rust, Javascript, Mathematica, Python, etc.

(Note that Lean 4, while still having some C++ core functionality, is moving heavily towards being implemented in Lean 4.)

Which programming language is used to implement a proof assistant is orthogonal to the language used by the proof assistant, although of course it might be harder to implement a proof assistant with Excel macros than in an ML-style language.

Answer 4

Because logic is a functional programming language

The point of a proof assistant isn't to write programs, it's to write proofs. For example, consider proving the statement $A \implies (B \implies A)$. Here's what a proof might looklike:

Assume A
 Assume B
  A
 Therefore (B -> A)
Therefore A -> (B -> A)

Doesn't look much like programming, does it?

Unless you're familiar with a specific type of programming called functional programming. Then you might notice that this is essentially lambda calculus.

λ A. (
 λ B. (
  A
 )
)

This correspondence is known as the Curry–Howard correspondence.

So it's not that proof assistant designers were like

Let's design a programming language for our proof assistant. Functional programming is my favorite paradigm.

They were like

Let's design a formal language for writing proofs. Also, due to the Curry–Howard correspondence it will also be a programming language (specifically a functional one), so let's borrow design principles from programming language design. In fact, we'll even let the user "run" the proofs as programs, since that's convenient.

There are some proof assistants that aren't based on functional programming, such as MetaMath. But they aren't OOP instead, they are not a programming language instead.