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



I'd like to understand why such a tool/setup doesn't exist.
Because of technical difficulties?
Because such projects won't be cool enough to publish in "top conferences"
and please the career gods?
I very vaguely remember hearing about attempts to make such tools, about
3-5 years ago. I'd love to hear their experience.

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/


On Thu, May 28, 2020 at 11:36 PM Heiko Becker <hbecker at mpi-sws.org> wrote:

> Hi Talia,
>
> I hope I am not too late to add my answer.
>
> We have a Coq and HOL4 codebase for our floating-point roundoff error
> checker FloVer [1]. However, the Coq and HOL4 versions have diverged
> quite a bit now where the Coq version has features that are not present
> in the HOL4 version, and vice versa.
>
> So I guess in a world of perfect interoperability I would love to be
> able to transport the formalizations, or at least results checked by the
> tool, from one theorem prover into the other.
>
> Cheers,
>
> Heiko
>
> --------
>
> [1]: https://gitlab.mpi-sws.org/AVA/FloVer
>
> On 5/18/20 1:42 AM, 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.