Re: [isabelle] [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine?



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
>
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.