[isabelle] In a world of perfect interoperability between proof assistants, what tools would you combine?

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?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.