I think that the aesthetic dislike of "everything is a set" is misplaced, because it misses a crucial point that people unfamiliar with formal untyped set theories often miss: Not every proposition in a logic needs to be (or, indeed, can be) provable. The specific encoding of, say, the integers need not be an axiom. It's enough to state that an encoding of the integers as sets exists, but the propositions `1 ∈ 2` or `1 ∩ 2 ≠ ∅` can remain unprovable. Whether they're true or false remains unknown and uninteresting (or, put another way, "nonsensical").

The advantage is, then, that we can use a simple first order logic, where all objects in the logic are of the same type. This makes certain things easier and more pleasant. That the proposition `1 ∈ 2` can be written (i.e. that it is not a syntax error, though it's value is unknowable) should not bother us, just as that the English proposition "the sky is Thursday" is not a grammatical error and yet is nonsensical, doesn't bother us. It is no more or less bothersome than being able to write the proposition `1/x = 13`, with its result remaining equally "undefined" (i.e. unknowable and uninteresting) if x is 0. If `1/x = 13` isn't a syntax error, there's no reason `1 ∈ 2` must be a syntax error, either.

That a proposition is nonsensical (for all assignments of variables or for some specific ones, as in x = 0 in 1/x) need not be encoded in the grammar of the logic at all, and defining nonsense as "unknowable and uninteresting" is both convenient and elegant. I think that some logicians overlook this because they're attracted to intuitionist theories, where the notion of provability is more reified, whereas in classical theories every proposition is either true or false. They're bothered perhaps less by the ability to write 1 ∈ 2 and more by the idea that 1 ∈ 2 has a truth value. But while the notion of provability itself is not reified in classical logics, unprovable propositions are natural and common. 1 ∈ 2 has a meaning only in a very abstract sense; the theory can make that statement valid yet practically nonsensical by not offering axioms that can prove or disprove it.

Indeed, this is exactly how the formal set theory in TLA+ is defined: https://pron.github.io/posts/tlaplus_part2

1 ∈ 2 is operating at a _different layer of abstraction_ than peano arithmetic is. It's like doing bitwise operations on integers in a computer program. You can do it, but at that point you aren't really working with integers as _integers_.