This doesn't seem quite right to me:

  In the modern academic practice, the question of where a particular idea came from, or whether an axiom is ontologically correct, is considered vacuous and out of scope. For the most part, you’re just handed a rulebook to play someone else’s game.

To be clear I think the standard intuitive semi-naive set theory is the correct approach for most math students. But it didn't work for me. I needed to see the axioms and formal language.

Oh man, that resonates with me. One of the constant frustrations for me was that once you get foundations in a topic, the rest follows, but the foundations are often full of things that are axioms under one metatheory and theorems under another metatheory. When they were axioms, I remember always being comfortable, like "sure I can assume things," but as theorems there's always that bit of "wait hold up you can't just do that without saying more."

The one that I remember most strongly that way was the unique mapping from the empty set/object/whatever as a theorem.