"Set theory" can mean different things. The looser interpretation of set theory is just using the intuitive notion of sets to model things. I think basically e

"Set theory" can mean different things. The looser interpretation of set theory is just using the intuitive notion of sets to model things. I think basically everyone is for that and learning these topics is definitely the lower hanging fruit. The usual formal interpretation of what Set Theory is Zermelo Fraenkel set theory, which is roughly first order logic with some axiom schema about how sets behave https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t.... I would be somewhat skeptical that this notion of set theory is all that practically useful to use, although people have managed (metamath). In my opinion, first order logic is great in simplicity a degree of automatability, but clunky and awkward in terms of expressivity. Usually the awkwardness of expressing yourself outpaces the automation, and at that point there may be such a mess that it would be terrible to do it manually Type theory and dependent types are different formalizations of intuitive set theory. In a sense, types are kind of sets. From a pure english perspective, the words are close to synonyms and in practice the analogy is pretty close. 3 being of type Int is intuitively like saying 3 is in the set of ints. Type theory seems to me to lead to a cleaner system of syntactic formal reasoning, which sounds esoteric except that syntactic reasoning is what computers have to do since we can't convince them with English paragraphs. And perhaps we don't want to, since English is ambiguous. I think the success Lamport alludes to is even though he bases the TLA+ system on ZFC in some sense, users stick to the fragment of very intuitive notions of set where perhaps your foundations don't matter so much and all should basically agree. This may be more of a pedagogical emphasis than a true difference in systems, since almost everyone interested in dependent types finds the parts that go off into the stratosphere the most interesting.