"I hope the math community has reached the point of realizing that we really need not one foundation of mathematics, but many, together with clearly described relations between them. Indeed at this point the word ‘foundation’ is perhaps less helpful than something else… like maybe ‘entrance’."
, John Baez http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html#c042716
"There are some problems with this sort of compromise where material and structural set theories cohabitate as equal alternative foundations. ... this kind of cohabitation model is actually not the best possible way to accommodate both the material and the structural perspective at the foundational level. ... what we end up doing is moving all the annoyances from both sides into the translation between the two ... it would be much more satisfactory to have a greater overarching foundation similar to Cantor’s universe that comprises both the material and structural views.", François G. Dorais http://dorais.org/archives/1135
"if you care about internalizing mathematics in nonstandard models — not only in order to prove formal independence results, as set theorists do, but because you care about the nonstandard models in their own right and you want to use internalization to prove things about them — then ETCS is your friend and ZFC is your enemy. Structural set theory — and its sister, type theory — is very well adapted to internalizing in many different contexts"
, Mike Shulman http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html#c042933
"with ZFC is that it allows things like ⟨0,1⟩⊆3 which make no sense mathematically. I can assure you, though, that after you write one piece of code in x86 assembler which rewrites itself as it runs that manipulating all objects as binary and manipulating all objects as sets make perfect sense. This is what annoys me, in some sense, that people have an issue that in a system which allows you to encode everything as sets you can write some weird junk. Equivalently, this would be baffling to those people that if you write a piece of code in Common Lisp then the code itself is just a list and the program can manipulate itself (easier than to do that in assembler, I have to admit).", Asaf Karagila
"I don’t like the hard line that certain things are meaningless, simply because this depends on the setting. I don’t object to the idea of saying that an expression is, for your current purposes, well-typed, since this just means you say nothing about non-well-typed expressions. I would say not “meaningless”, but rather “does not have an intended meaning”. There are expressions, such as 0∈1 that do not have an intended meaning. If they have a meaning in a certain setting, then so be it.", Walt http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html#c042992
"ETCS is one, but apparently not one that is very congenial to many traditional set theorists, for a variety of reasons, maybe one being that many set theorists “don’t like categories” (well, okay, but again I think that’s a pity). Maybe some set theorists don’t like the privileging of functions over elements (although one take is that functions are generalized elements).", Todd Trimble,
"The same arrows aimed at ZFC can be easily turned at ETCS. It is equally easy to ask about “senseless things” which happen in ETCS but not in general mathematics. And this is not a critique against ETCS, but rather against the critique aimed at ZFC.", Asaf Karagila http://karagila.org/2013/on-leinsters-rethinking-set-theory/#289
"the issue is that first-order logic is not “type safe”, and I would suspect that people who have had exposure to first-order logic take this for granted, while those who have not may find it surprising. The reason is that syntax, in first-order logic, is defined independently of semantics, so that whether a formula is well-formed (syntactically correct) is independent of what the formula means. ... This issue of “type safety” arises also in programming languages. Some languages, such as C, have little run-time type checking. I can take a 64 bit integer and treat it as an array of eight 8-bit characters – with implementation-defined results. ... In working mathematics we have humans to check that the formulas we actually write make sense – nobody accidentally writes 1∈sin in an analysis paper – so it is not clear that there is any real advantage to stronger “type checking” in the foundations.", Carl Mummert http://karagila.org/2013/on-leinsters-rethinking-set-theory/#274