&gt; If you want a formal proof in the typical sense of the word (rather than a verification of fact based upon model checker output), then Coq userlands&#x27;s tactics and theorems are useful.<p>TLA+ has them, too.<p>&gt;  in-so-far as one realizes that other people might have different experiences and so might (just as validly) consider other formalisms more familiar.<p>So you think some people are more familiar with type theory than with undergrad-level set theory (ZF)?<p>&gt; sometimes, the type theoretic approach really is simpler, more familiar, and more flexible. E.g., in the case of this dissertation<p>I don&#x27;t see it (probably because my type theory is very, very basic; I&#x27;m an algorithm&#x27;s guy and the thought that a data-structure of mine might need type theory to be specified makes me shudder), as in I fail to see anything that isn&#x27;t readily expressible in simple classical logic + temporal logic. Could you explain?