Yeah, my point is exactly what you say at the end - for practical applications, those theoretical details (which are enormously challenging) generally aren't necessary, and the problems they address aren't the ones application practitioners will encounter. I definitely understand the motivation for theoretical structures within math itself, and i have no issue with e.g. the axiom of choice for people doing mathematics itself.