The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

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
>