One may argue that formal set theory relates to topos theory in the way that untyped lambda calculus relates to the typed theory. If you think it's difficult to get a model of set theory out of a topos try to get a model of untyped lambda calculus out of a model for the typed theory. The semantics of core mathematics -- unlike the semantics of a programming language -- has never presented much of a problem. The perversity of formal set theory as a foundational language for mathematics has not been much in evidence for the simple reason that no mathematician has ever actually used it for his semantics. I am not saying here that the continuum hypothesis is perverse, or even questions about much larger cardinals. (For one thing they can be stated easily in a topos setting.) I am saying that formal set theory allows entirely perverse questions that have nothing to do with the semantics of mathematics. The actual elements used for a mathematical construction are never of interest. Imagine your reaction to an interruption at the beginning of a lecture on number theory, "Which construction of the natural numbers do you have in mind? Russell's or Van Neumann's?" My favorite example of the sort of perverse question one can ask if one were to take formal set theory seriously is "Does any simple group appear as a zero of the Riemann Zeta function?"