Hacker News Reader

Agreed; e.g. if you prove something about the real numbers, the matter of how R is constructed out of your axiomatic system doesn't matter

The picture isn't quite so clean in the constructive context, which is what many of these proof systems are rooted in, e.g., https://mathoverflow.net/questions/236483/difference-between...

there are questions where the abstraction of real numbers becomes leaky, and some axioms (or their lack) poke through.