Tackling the second part first: Yes, mathematicians use all sorts of reasoning in pursuit of mathematical truth. Sometimes this reasoning is mildly sloppy, or abuses notation. So what? We all know in principle that this reasoning can be written down formally in ZFC with enough effort, if we really needed to, and this is enough to satisfy us. If you go to a mathematician and claim their work in number theory isn't actually rigorous because they wrote "7" to mean the equivalence class of 7 mod p, instead of a separate symbol like a 7 with an overbar, they will laugh at you.

> But the whole point is how to keep track of what questions one is evidently allowed to ask - what questions are demonstrably not as ill-posed as "is the number 7 equal to the trivial group".

I don't understand what you mean by "questions one is evidently allowed to ask." You can ask any questions you want. In particular, as long as we agree that whatever question you want to ask can be translated into a question about sets, we can resolve that question by answering the analogous question in the framework of ZFC. All I object to is the claim that some set is, ontologically speaking, the same as the number 7, and hence that set theory proves "junk theorems."

Here's a silly analogy. Suppose we work at NASA and we want to fly a rocket to the moon. We agree that the answer the question of how much fuel we need, we can write a computer simulation with a representation of the rocket, the earth, the moon, and so on. We run the simulation and answer our question in that simulation, and if the simulation is a good representation of reality that also answers our question in reality, and then we go to the moon and everyone is happy. However, nowhere in this process do we believe that the rocket in the simulation is the same thing as the rocket IRL.