3 ms·

I would like to get into formal methods but I am kind of confused. What's the difference between TLA+, Coq & Isabelle? Is there one should I prefer over the o

by max_ 6y ago

I would like to get into formal methods but I am kind of confused. What's the difference between TLA+, Coq & Isabelle? Is there one should I prefer over the other? Or do they individualy satisfy distinctive purposes?

zaik 6y ago
I am no expert, but Coq and Isabe le "feel" very similar at first, but Isabelle seems to provide much more powerful tools for proof automation than Coq. Isar, Isabelle's proof language, tries to be close to natural language proofs which makes it more intuitive. I really wish Coq had equally powerful automation tools and a more intuitive proof language, because it feels much more of a solid language and I really liked that the clear relation of types <-> statements, terms <-> proofs, type checking <-> proof verification; including the ability to print the raw proof terms of theorems.