So, as far as I'm concerned, real analysis depends quite largely on some weak variants of the axiom of choice (such as the axiom of countable choice), and there seems to be no controversy surrounding this use of the axiom of choice. However, there has been significant criticism of nonstandard analysis (such as the notorious criticism by E. Bishop). My question is: do these criticisms come down to the fact that the construction of the hyperreal numbers depends on a lemma whose strength is on par with that of the axiom of choice (Zorn's lemma)? Or does it boil down to another reason?
Additionally, in response to Bishop's review, Keisler asks "why did Paul Halmos choose a constructivist as the review [of A. Robinson's Nonstandard Analysis]", which also stokes the question: how does the axiom of choice impede on constructive proofs?
I would much prefer answers in lay terms, but any help is equally appreciated. Thank you.