That's a flawed analogy. Mathematicians do use 'higher level languages', that's precisely why most of them don't care about HoTT vs set theory. Just like a web dev usually does not care about the instruction set of the processor.
Its not flawed because the correct analogy is: pen and paper Turing machines versus Python.
Now I'm not sure what your point is. Are you suggesting that HoTT is to python as ZFC is to turing machine tape?
Nah the math people are fine with assembly, even though they don't actually use it in their work.