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