4 ms·

I'm a referring the guys paper, which is linked here in the comments somewhere. There TLA+ is mentioned which is a tool to formally prove something. The same ca

• tel 12y ago
  While that parallel is genuine, it's hard to compare Coq and TLA+ since the mechanism and style of proof they embody is very different. TLA+ tries to ensure that you can exhaustively check implied models as its basis of proof (I believe) while Coq recognizes that types syntactically represent logics and we can thus construct programs in those logics to represent proofs. So, one layer deeper they're dramatically different beasts.
  • swatow 12y ago
    you are correct. There is a huge difference between the two and as you say only coq is able to express proofs in themselves and not just a coarse grained summary of their structure.
  • grogers 12y ago
    The TLA+ tools can do exhaustive model checking, as well as mechanically checked proofs. The proofs typically use an SMT solver to verify them. Of the two I've only used model checking in a serious way, but you can find Lamport's proofs of things like paxos and have it turn all the theorems green.
    • tel 12y ago
      SMT is still a pretty far cry from type theoretic proof. At the end of the day it's just another kind of exhaustiveness checker.