<i>&gt; TLA+ has them, too.</i><p>Like I said, modus operandi matters. If I have to perform another model checking routine (possibly on an infinite state space) to slightly generalize a theorem, then in many cases that means I never really had a useful proof of it in the first place.<p>Also, Coq&#x27;s mathematics library is extensive and often closely follows the proofs found in graduate mathematics text books. Last I looked into TLA+, it was squarely focused on algorithms and hardware (not even CS-related mathematics more generally -- specifically algorithms and hardware).<p><i>&gt; So you think some people are more familiar with type theory than with undergrad-level set theory (ZF)?</i><p>Do I think there exists some population of people who are &quot;more familiar&quot; with type theory than with ZF? Yes, starting, for example, with every researcher whose primary area of study is type theory. In fact, I think that anyone who doesn&#x27;t honestly believe there are such people must have an extremely low opinion of quite a number of very smart people.<p>(Also, set theory qua set theory gets really disgusting and kludgey really quickly, and is something that almost no undergraduate (or even phd student) is exposed to these days. The &quot;set theory&quot; you see in a discrete math course kind of barely scrapes definitions. I think most people who posit that &quot;set theory&quot; is nice and simple must&#x27;ve never really dove deem into the actual theory of set theory...)<p>(Also, most real math these days quickly abstracts away from germanely set theoretic constructions. Mathematicians don&#x27;t work in ZF. They do not. Most will <i>tell you</i> they do not, if they even know what ZF is. Which a lot won&#x27;t, because their undergrad discrete math course is probably the last time they saw a truly formal derivation. And the mathematicians who do know what ZF is often can&#x27;t regurgitate an axiomatization of ZF. If you tell a mathematician that all of math is just set theory, most will chuckle and wink and say &quot;why, yes, yes it is&quot;, and hopefully you&#x27;re in on the joke...)<p><i>&gt; I don&#x27;t see it... I fail to see anything that isn&#x27;t readily expressible in simple classical logic + temporal logic. Could you explain?</i><p>Did you read this dissertation&#x27;s explanation of why separation logic is important?<p>To the extent that this observation is remotely reasonable, it&#x27;s only in the sense that you can code up one logic in another. Which, well, all the world&#x27;s a TM, as they say...<p>Anyways, I think the argument over whether type theory is a successful foundations for CS research and practice is already a closed issue. It demonstrably is. So is set theory.