What are the strengths and weaknesses of the Isabelle proof assistant compared to Coq?

Question

Does Isabelle/HOL proof assistant have any weaknesses and strengths compared to Coq?

Answer 1

I am mostly familiar with Coq, and do not have much experience with Isabelle/HOL, but I might be able to help a little bit. Perhaps others with more experience on Isabelle/HOL can help improve this.

There are two big points of divergence between the two systems: the underlying theories and the style of interaction. I'll try to give a brief overview of the main differences in each case.

Theories

Both Coq and Isabelle/HOL are based on powerful, very expressive higher-order logics. These logics, however, differ on a few features:

Dependent types

Coq's logic is a dependent type theory, known as the calculus of inductive constructions (CIC for short). "Dependent type" here means that types in Coq can refer to ordinary values. For instance, one can write a matrix multiplication function mult with type

mult : forall (n m p : nat), matrix n m -> matrix m p -> matrix n p 

The type of this function says that it takes two matrices as inputs, one of dimension n x m and another one of dimension m x p, and returns a matrix of dimension n x p. The theory of Isabelle/HOL, on the other hand, does not possess dependent types; hence, one cannot write a mult function with the same type as the one above. Instead, one would have to write a function that works for any kind of matrix, and prove a posteriori certain properties of this function when it receives arguments of the right kinds. In other words, certain properties that are manifest in Coq types need to be asserted as separate theorems when working on Isabelle/HOL.

While dependent types are interesting for some things, it not clear how useful they are in general. My impression is that some feel that they are very complicated to use, and that the benefit of having certain properties expressed at the type level versus having them as separate theorems is not worth this additional complexity. Personally, I like to use dependent types in few cases, when there is a clear reason to do so.

Basic reasoning principles

Coq's theory by default lacks many reasoning principles that are commonplace in mathematical practice, such as the law of the excluded middle (i.e., the ability to reason non-constructively), extensionality (for instance, being able to say that functions that produce equal results are themselves equal), and the axiom of choice. In Isabelle/HOL, on the other hand, such principles are built-in.

In theory, this is not a big problem, because Coq's logic was designed to allow people to safely add these reasoning principles as extra axioms. Nevertheless, I have the impression that it is easier to do this kind of reasoning on Isabelle/HOL, since the logic was built from the ground up to support them.

(You may wonder what the reason is for leaving such basic principles out of Coq's logic. The motivation is philosophical: in Coq's core logic, proofs can be seen as executable programs, which gives the logic a constructive flavor. The reason for rejecting the excluded middle, for instance, is that the proof of a disjunction A \/ B corresponds to a program that returns a bit indicating which one of A or B is true; thus, the excluded middle would correspond to a program that decided every mathematical question, which cannot exist. This question discusses the issue a bit further.)

Style of interaction

Both Coq and Isabelle/HOL are interactive theorem provers. They are languages for writing definitions and proofs about them; these proofs are checked by a computer to ensure that they have no mistakes. In both systems, one writes down a proof by giving commands that explain how to prove something. The way this happens on each system, however, varies.

Isabelle/HOL generally speaking has more mature support for "push-button" proof automation. For instance, it comes with the famous sledgehammer tactic, which invokes several external automatic theorem provers and solvers to try to prove a theorem. Coq also comes with many powerful proof automation procedures, such as omega or congruence, but they are not as generally applicable, and many theorems that can be solved with a single command in Isabelle/HOL require more explicit proofs in Coq.

Of course, this convenience comes with a price. I've been told that it is harder to have control over one's proof in Isabelle/HOL because the system tries to do a lot by itself. This is not a problem when proving simple theorems, but it becomes an issue when proof automation is not powerful enough and you need to tell the theorem prover how to proceed in greater detail.

The situation is a bit different when supporting user-defined, proof-automation procedures. Coq comes with a tactic language for writing proofs, known as Ltac, that is a programming language of its own right. Even though Ltac has some design problems, it does allow users to encode fairly complicated proof automation procedures in a lightweight manner. For heavier tasks, Coq also allows users to write plugins in Coq's implementation language, OCaml. In Isabelle/HOL, in contrast, there is no higher-level automation language like Ltac, and the only way the user can program custom proof automation procedures is with plugins.