> Interop is hard, because all the axiom systems tend to be subtly different in ways that are hard for normal people to appreciate, though there is some work on it, including MM0.

Would it be tenable to build a parameterized axiom-system-evaluation-engine for which the semantics of a specific proof-assistant would consist of a configuration for this general engine, rather than patches to its code?

If so, would it then be possible for interop to happen "between" proofs in slightly-different axiom systems, the way that regular hand-written "translational" proofs work in mathematics — i.e. "take this property we've proved, translate it into domain model X, derive a property Y, then translate property Y back out of domain model X and into domain-model Y, where we actually want to use it?" — but all under-the-covers, as the (proven) equivalent of FFI, autogenerated as glue proof-code by analyzing the differences between two "configurations" to the engine?