Ok, there are a number of points you can make comparing set theory and type theory... but the most important point here is that it is a false dichotomy! From a

Ok, there are a number of points you can make comparing set theory and type theory... but the most important point here is that it is a false dichotomy! From a logical point of view "type theory" is a particular formalism for describing logical frameworks. ZFC is the "type theory" of first-order predicate logic plus a few axioms which add a type of sets, a predicate for set membership and assert certain properties of set membership. You can add function types to ZFC and you do obtain a strictly stronger system (Higher-Order ZFC). The main practical advantage is that you do not need to encode your problem into first-order logic. For instance, in higher-order set theory a (very strong) form of the axiom of choice asserts that there is a function "epsilon : set -> set", such that "epsilon x \in x" for x not empty. Expressing the same in first-order ZFC turns the whole statement on its head since you need to encode this function somehow. This leads to (almost) equivalent but misleading statements, such as "the intersection of a set all of whose inhabitants are non-empty is non-empty". Now if you look into TLA+, you will find that this choice operator epsilon has been added to the language, because it is so useful in practice! And this is just one instance of something that "type-theory" can add over classical ZFC. More to the point, higher-order specifications are crucial for the verification of higher-order programs. Higher-order programs are in turn one of the most useful tools for writing modular code. Sorry for the nitpicking; let me get back on topic. The main advantage of Martin-Löf style type theory is that it makes it easy to build new abstractions. For instance, the Bedrock project (http://plv.csail.mit.edu/bedrock/ http://plv.csail.mit.edu/bedrock/) builds an extensible program verification environment within Coq. This is only possible because the underlying logic is so expressive that you can build internal models for whichever pet logic you want to reason in. From a practical point of view dependent types and the conversion rule - computations in proofs - allows you to build scalable (reflective) proof automation while retaining a small trusted base. The constructive aspect of Martin-Löf type theory is very pleasing from a philosophical point of view, but again in practice it's not the most relevant aspect. The main reason for me to use something other than classical logic is that there are more models of intuitionistic logic than of classical logic. This gives you more freedom in designing a logic which makes it easy to reason about your particular problem domain. For instance, if you work with Cyberphysical systems, you might like to work within the framework of synthetic differential geometry where all functions are smooth and the real numbers are as simple as they can ever be. What so many people seem to be ignoring is that the logic you use for reasoning is part of your design space. Saying "I'll just use ZFC" is exactly the same as a programmer exclaiming "I'll just use COBOL". Leslie Lamport designed TLA+ to make it easy to reason about distributed systems. There may well be a nicer logic for reasoning about distributed systems, but you will probably not find it among the models of classical ZFC, since there aren't really that many of them... On the other hand, there are many different flavors of type theory, just waiting to be discovered. And in my view that's the main advantage of looking beyond set theory.