3 ms·
How is interoperability going on between those various formal systems? Couldn't we devise some common intermediate representation, or API? Some languages (and
by MayeulC 7y ago
How is interoperability going on between those various formal systems? Couldn't we devise some common intermediate representation, or API?
Some languages (and their approaches) are probably better suited to some mathematical objects, like some demonstrations are easier to perform algebraically than geometrically, for instance.
- raphlinus 7y agoThis turns out to be quite hard, because there are irreconcilable differences in the fundamentals of the different proof systems. That said, there's the Dedukti project, which is showing promising interop results between (at least) Coq and HOL style logics, and the work Mario Carneiro is doing trying to bridge between Metamath and more type-theory approaches.