To build upon the "Just relax" section: by Shoenfield's absoluteness theorem[1], if ZFC proves some Sigma^1_3 statement, then ZF also proves it. In particular, the Axiom of Choice has no arithmetic consequences, and thus has no effect on number theory, nor what you are able to prove about the correctness of any particular algorithm, etc.
This is super cool and I wish I'd known about it before writing the piece; I'd have been comfortable being a lot more muscular in the conclusion. This seems like it makes precise my suggestion that the axiom of choice only matters for aggressively infinite and unphysical statements.
[1] https://en.wikipedia.org/wiki/Absoluteness#Shoenfield's_abso...