4 ms·

Thank you very much for the answer! Could you elaborate on the last (now first, after edit) point you made? Sorry if the question is naive, I don't know much a

• seanwilson 6y ago
  So picture trying to take a C snippet and using it inside a JavaScript project. On top of the different language syntax, each language has different definitions on equality, strings, arrays, numbers, control flow, pointers etc. so there's no simple mapping that would let you translate the C snippet into a snippet a JavaScript interpreter would understand and if you're not careful with your mapping you're going to get bugs. Similarly with theorem provers, on top of just the syntax, they each have their own definitions for equality, data structures etc. that don't have simple mappings, as well as differences in the basic proof axioms all proofs must be built on. Both specifications and their proofs won't map easily between theorem provers which you'll have to reconcile somehow.
  • cloogshicer 6y ago
    Thanks for the explanation!