The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

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
>