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



Just for clarity, I said "tools" which was a bit ambiguous, but I meant
more along the lines of what Gerwin wrote. Appreciate the useful thoughts
from all regardless :)

On Sun, May 17, 2020, 9:03 PM Tadeusz Litak <tadeusz.litak at gmail.com> wrote:

> Isabelle:
> + Sledgehammer
> + Archive of Formal Proofs
>
> Abella, Beluga or Nominal Isabelle:
> + Ease of dealing with binders and freshness
>
> Agda or Coq
> + Not forcing classical metatheory down your throat
> + Dependent types
> + Being based on a functional programming language
> + Type classes
>
> Agda
> + Dependent pattern matching done properly
>
> Coq
> + Ability to go impredicative
> + Rich tactic languages, including ssreflect
> + Libraries and community
>
> And it would all have to be implemented as efficiently as Isabelle or Coq
> is.
>
> Apologies if I am missing advantages of other proof assistants, or not
> doing full justice to those already mentioned.
> These are just first things that came to mind based on my very limited
> knowledge and experience.
> t.
>
> On 18.05.20 01:42, Talia Ringer 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.