Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
    < Chronological >      < Thread >
  • From: Tadeusz Litak <tadeusz.litak AT gmail.com>
  • To: coq-club AT inria.fr, Talia Ringer <tringer AT cs.washington.edu>, isabelle-users <isabelle-users AT cl.cam.ac.uk>
  • Subject: Re: [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine?
  • Date: Mon, 18 May 2020 06:03:05 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tadeusz.litak AT gmail.com; spf=Pass smtp.mailfrom=tadeusz.litak AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f42.google.com
  • Ironport-phdr: 9a23:ftVMABDEISmTT2MFkv20UyQJP3N1i/DPJgcQr6AfoPdwSP37osqwAkXT6L1XgUPTWs2DsrQY0reQ6vi8EjNdqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5yIRmssAndqsYbjYRgJ6sx1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOiUn+2/LlMN/kKNboAqgpxNhxY7UfJqVP+d6cq/EYN8WWXZNUsNXWidcAI2zcpEPAvIbPehFsYf9qVsAoxiwCwaiC+zgyCNHiHDt0K0m0eksCx3K0BAuEt8MtnnfsdX7NL0VUeCw1KTG0y/MYO5I1jfg84jJcw0qr/eNXbJsa8XRylQkGgTZjlqKtIPqIS6V1v8MsmSB6+pgVP6vhHQkqwxqrTivw90jiojNho4P1l/E8iB5zZ8zKNalR0F1fcSqH4FMtyGGKYR2WMUiTnlqtSs6yLALt4O2cDUXxJg52hLSb+GKf5SL7x7+SeucISp1iXBkdb+9iBu/80eux+zzWMSpzFpHrzZInNfNu30P0RHY98uJSuNl80u/xTqC0xrf5+JELEwui6bXNYMtzqQ/m5YNqUjPADP6lFnrgKKTa0kp+/On5ufib7n4u5CQKYF0hwT6P6syhsCzHeE1PwwSUGWU+Omx0aPs8ELlTLhPjvA7najUv47fKMsFpqO0AwxY34A+4BilFTimys4XnXwfIVJFZh2Hi4/pNknLIP/iDPe/h02gkTlxx/zbJ7HhDJrAImbZnLfuerZ97EFcyA4twtxF+51UDbQBLOryWk/3qtPYEgc0PxKoz+vjEtlw1YMTVXiRDqOHLa/eq1CF6vw3L+mJfoAVuTL9K/Y/5/7piH80gUMdcrO00pQJdXC4BfVnL1+dYXrtntcOC2QKsxExTOzvklKCUDpTa2yuUKI74zE3EJimApvbRoCxnLyB2z+2EYFRZmBfE1yDDXPod5ifVPoXcyKTIsphkiQeWrS7So8h0wuutA7gxLZ9IOrU4H5QiZW2399soubXiBsa9DpuDs3b3XvJB119mmIBDwU32q9yuwQp1k2C16d1mdRTDppM7uhJUwE1KZnaieF2Foa2EgPad92ETFKrB8i9DCsqBoYw2NYEbkJ5FpC/lR3ZxAKhB/kenrnNDZdy76GKjEL8P8Js93GTyKAtgkQ9UI1LNHGvhYZw8gHSA8jClEDKubytcPEg1SLA6XyRhU6PoEhbGFpsWKnIQGsNIE/Xsd36zkzHRr6qT78gN10Smoa5NqJWZ4ix3h19T/D5NYGbOjrpwjviNVOz3rqJKbHSVSAFxiyEURoLlgkS+TCNMg1sXn788VKbNyRnEBfUW22p8eR6rynmHEo9zgXPcFc4krTpoFgagvuTT/5V1bUB6n94+mdEWW2l1teTMOKu4g9ofaFSe9Q4uQ4V2mfQtgg7NZulfflv
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



Archive powered by MHonArc 2.6.19+.

Top of Page