<i>&gt; TLA+ is not a model checker. It&#x27;s a specification and proof language. There is a model checker that can check TLA+ specs, just as there is a proof assistant that can check TLA+ proofs.</i><p>For the third (!) time, modus operandi matters.<p>Coq&#x27;s huge library of tactics and proofs of facts that TLA+ might just throw at a model checker are, in my experience, very useful starting points for things that can&#x27;t be model checked.<p>Ostentibly TLA+ could build up an equivalent library of tactics and proofs.<p><i>&gt; Why low opinion?</i><p>Even supposing type theory is &quot;more obscure&quot;, it&#x27;s pretty hard to believe that someone could study it for 30 years and not understand it better (in some sense) than ZF. That&#x27;s a pretty extraordinary claim.<p><i>&gt; basic set theory -- the one that barely scrapes the definition -- is all that&#x27;s required to specify real-world programs.</i><p>Not really -- you often need non-trivial constructions when proving properties about rewrite systems within set theory. Those constructions are <i>much</i> harder to understand than induction on algebraic datatypes, which is why type theoretic approaches have dominated in formalization of programming languages.<p><i>&gt;Unless I&#x27;m missing something...</i><p>I&#x27;m disinclined the dismiss separation logic just because you can code up some of its ideas in another logic (in a way that counts as a novel contribution worthy of publication, no less).<p>The clarity with which separation logic presents the idea and use of the separating conjunction has obviously influenced the paper you cited. I would think this is reason enough to summarily dismiss these &quot;everything&#x27;s a TM&quot;-style arguments you&#x27;re making here. The authors of the paper you cited are only not using separation logic in a kind of meaningless sense IMO.<p><i>&gt; So far, I don&#x27;t see why I should.</i><p>This sentiment kind of reminds me of people who have never typeset mathematics complaining that LaTeX is useless... which is to say, perhaps you simply aren&#x27;t interested in and so don&#x27;t care about the use cases where Coq shines? Lots of people -- including me -- have already pointed out a lot of these use-cases in this comment section.<p>But really, based on the arc of this conversation, I would be enormously surprised if you chose to use Coq to prove X, even if there were a proveX tactic already written in Coq and the TLA+ implementation would take all day ;-)