I don’t believe in historical accidents. We “ended up” with set theory because it’s an incredibly rich system that has powered almost every important mathematical discovery in the last 150 years.
We use it because it is the most effective tool for formal reasoning that human beings have ever come up with. The fact that it has limitations, especially in the new world of computation, does not take away its utility.
To me, sets seem like the much more foundational idea, since types were only suggested as a fix for Russell’s paradox. Almost all math can be done without ever running into the limitations of Russel’s paradox, so I look at type theory as more of an evolution of the understanding of sets than anything else.
We use it because it is the most effective tool for formal reasoning that human beings have ever come up with. The fact that it has limitations, especially in the new world of computation, does not take away its utility.
To me, sets seem like the much more foundational idea, since types were only suggested as a fix for Russell’s paradox. Almost all math can be done without ever running into the limitations of Russel’s paradox, so I look at type theory as more of an evolution of the understanding of sets than anything else.