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


I would like to see Compcert, at least its backend (IR, optimizations,
machine code generation), being usable from Isabelle. 
Then I could probably retarget my Refinement Framework to use Compcert-
IR as a backend, closing the gap from very high-level specifications to
machine code. Similar for CakeML (Currently, the Refinement Framework
targets LLVM or SML).


On Sun, 2020-05-17 at 16:42 -0700, 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.