Set theory basically is the same thing as type theory, these are two schools of formal languages designed to define logics (something which is even more true fo

Set theory basically is the same thing as type theory, these are two schools of formal languages designed to define logics (something which is even more true for this book that seems introductory). I don't really like set theory (imho it's a pain to use rigorously formally) but type theory is cool. If you've already used typed languages in the ML/haskell family you will have a lot of intuition in constructive logic (formal reasoning in type theory is literally the same thing as programming). Shallow applications of type theory are numerous in recent developments of compilers (using types, rust can manage memory correctly and statically; in general types are a good channel between humans and compilers for high level and structured information about what they are writing, leading to tons of systematical optimizations). So: all kinds of typed programming languages with non trivial features being effects (monads&modalities, linear logic), structuring/interfaces (parametrized modules, type classes, translucent types, ..) or interactive theorem proving.