The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

Isabelle seems to really shine in proof automation, but obviously it doesn't hold much of a candle to automated theorem provers like Vampire, Z3, Minisat, ACL2 (to a certain extent) etc.

Coq has the remarkable advantage that a lot of it's extra structure, type classes, proof witnesses, computational reflection, come for free within the kernel (with the notable exception of modules). Of course this kernel is quite complex, almost the opposite of HOL-light's, which is remarkably trustworthy.

Almost every widely used tool has unique libraries and tactics which are found in no others, of course.

It's hard to tell which of these differences are intrinsic tensions of the tool designs and which are incidental. Contrary to similar debates about programing languages, however, it seems that every one of these can be embedded in some, reasonably trustworthy, super-logic, roughly on par of ZFC + largish cardinal axiom. At the cost of some severe foundational debates though, I guess.

Logics which are really useful and popular right now are linear, modal and seperation logics, which have to be embedded into such a system along with a proof of soundness if you want the same level of trust. This is usually extremely tedious, at least given my limited experience, both WRT notations and proof conveniences. I've seen several examples of systems originally designed as a deep embedding which were then turned into standalone tools because of this tension (CertiCrypt springs to mind).

I'm not sure this tension can be resolved, since there is no common ground in this case (to my knowledge). Twelf might make such a claim as a unifier, but it is a very thin veneer over the astronomical amount of work required to make the logic even remotely usable. There's a reason why in 99% of cases the word "Isabelle" is followed by "/HOL". Logical frameworks have so far not lived up to their promise.

As is usually the case in the PL world, usable languages are often usable because of the quality of the libraries, and their ease of installation. This is largely a language specific effort, unfortunately. This makes me something of a pessimist, as in most domains, but I guess someone's got to occupy that quadrant.

Thanks for the opportunity to rant,

Cody

On Sun, May 17, 2020 at 7:43 PM Talia Ringer <tringer AT cs.washington.edu> wrote:

Say we one day are able to just take things from Isabelle/HOL and use them with Coq developments with no additional effort, or similarly in the opposite direction, or similarly for any other pair of proof assistants. Say we would get strong guarantees about these combined verified systems. Just humor this for a second.

In such a world, what systems would you want to combine, and why?

Talia