There's a lot of mathematics which can't be formalized in classical first-order logic with the ZFC axioms. For most things you can get around this by adding enough Grothendieck universes, but this is still incomplete and always will be.
Set theory is a reductionistic system. It's supposed to give a foundation which is as "small" as possible.
In set theory you start with almost nothing and you have to encode all useful concepts into sets before you can start proving/programming.
Compare this to Turing machines, where you start with a very primitive model of computation. The first step in most treatments of Turing machines is similar to set theory, you show that some useful concepts (associative memory, high-level control flow, etc.) can be encoded into Turing machines. You then use this encoding to construct arbitrary programs.
Type theory starts out with a functional programming language and you derive new concepts from free constructions. In type theory you shouldn't be encoding things at all. You should be describing concepts (~adding an API) and possibly extending your model (~the compiler).
As analogies go, I'd say that this one is pretty accurate.