Newbie question: if one is not interested in extracting programs, but only in proving stuff, is a proof assistant like Isabelle/HOL easier to use than one based on constructive logic like Coq?
The short answer is yes. That's because (1) a classical system like HOL can use external automatic theorem provers ("sledgehammer") that are based on classical logic (most of them are), in a way that constructive systems like Coq cannot (at least currently). Moreover (2) classical proofs can be shorter and simpler, sometimes considerably so.
In practise many other dimensions also play an important role, in particular available tactics, tactic definition languages, proof editors, available decision procedures for the specific axioms one is interested in, libraries and so on.
Although Coq is using constructive logic by default, it is not limited to it. One can use classical logic results just by importing the "Classical" module. Or course one then loose the benefits of having a constructive proof (like code extraction), but if the interest is only in checking a mathematical proof then it can be acceptable. The choice and trade-off is up to the user.
That is true, but does proof automation work as well for classical reasoning in Coq as it does in Isabelle/HOL where classical reasoning is 'baked in' from the start?
As far as I'm aware, the question of moving the "sledgehammer" approach to a constructive setting is still an open problem.
If you are interested in program
verification, then not all that much, because everything is about
automation. Coq/Agda have a small edge if you want to prove something
about Lambda calculus since Coq/Agda are themselves Lambda calculi,
and not surprisingly most Coq/Agda work is about Lambda calculus
... The HOL school has probably a small edge in other areas.
In practise the underlying approach (LCF vs Curry-Howard and dependent
types vs HOL) makes much less of a difference than automation and
availablility of proof libraries.
I'm not sure I agree. For example CakeML [1] is the first fully verified self-hosting compiler for a substantial programming language, and seL4 [2] is the first fully verified substantial operating system kernel. Both were verified in LCF provers using HOL as a logic. Are you saying that the guarantees of correctness are not in themselves useful?
If I write a program X and tell you it was proven correct, do you know that X is useful?
To know that a correct program is useful, you have to know what it does. And if you know what it does, you have constructed an implementation.
Which is to say that a nonconstructive verifier is really just deferring the 'constructive' part of its operation to the compiler and programmer. (And this is the 'hard part' I was referring to.)
We are discussing the (dis)advantages of HOL vs constructive reasoning (e.g. Coq). The main
difference is that HOL-based provers like Isabelle/HOL has
classical built in from the start -- all proof automation supports classical
reasoning. Constructive reasoning eschews classical methods.
In order to prove the correctness of a program X, I need a
specification S, and then I construct a proof P that X |= S, i.e. that X
satisfies the specification S. I use an interactive proof assistant
to check the proof P. There is no disadvantage that I can
see if the proof P of X |= S is classical, at least from the point of
view of program correctness.
