I am really tired of all the propaganda which says that the axiom of choice is this necessary evil, because it is really useful in proofs but the choice functions are not constructive. Because yes, the axiom itself gives you no scheme for constructing an explicit choice function. That much is true. But I would argue that the axiom's negation is actually way more non-constructive!
The axiom of constructibility (also known as V=L) implies the axiom of choice, so the negation of the axiom of choice implies the existence of sets which are not ordinal definable, and thus cannot be constructed by exclusively appealing to the axioms of ZF (which, with the exception of extensionality and foundation, are all axioms which exclusively describe closure properties of the set-theoretic universe).
In fact, the proof of V=L implying choice is constructive! If V=L holds, we can explicitly define a well-ordering of the entire set-theoretic universe! Not only that, but the existence of a transitive model of ZF implies a transitive model of ZF+V=L which is point-definable, i.e. every set in that model is uniquely characterized by a first-order formula of set theory. Every set being definable strikes me as very constructive.
Sure, things like Banach-Tarski are pretty weird results that require the axiom of choice or a similar axiom. But the only real issue here is that we ascribe our geometric intuition to a partition of a sphere that is impossible to do in real life! Not only can we not divide real-life objects infinitely often, but even if we could, we physically could not select points the way that Banach-Tarski requires.
I think it is interesting to think about set theories where choice does not hold or may not hold. Certainly, a set theory where all subsets of R are measurable is appealing, if only for convenience. And it is legitimately fun to prove equivalences between the axiom of choice and various other propositions, such as the total ordering of the cardinals or Tychonov's theorem, or to reason about the relative strengths of different weaker variants like dependent choice, or my personal favorite, the ultrafilter lemma. It gives you more insight into the beauty of choice. But, in as much as you can 'believe' in an axiom, I believe that the axiom of choice is true in the platonic ideal of mathematics, and I will not stand for slander against it.
So... this post was right and wrong. I still stand by my dunking on those classical mathematicians who dislike choice, but I was operating on a notion of 'constructive' that is as nonsensical as a classical mathematician's objection to the axiom of choice (hint hint: they are the same thing). The only correct notion of constructive is one based in working in intuitionistic logic. The proof of the existence of a global well-ordering of the universe makes very heavy use of excluded middle, a non-constructive logical principle.
The idea that a result is explicit so long as it avoids the axiom of choice is immensely naive. In fact, in Bishop-style constructive mathematics, the axiom of dependent choice (a weaker variant) is even a theorem.
Really, the issue with the axiom of choice is that it says an obvious, objectively, trivially true thing... as long as we work in a suitable type theory and are talking about proof objects rather than extensional functions. But the set theorist knows only extensional functions, not proof objects, so they misapply their intuition.
On the other hand, if you already accept excluded middle, you should just go all the way. The axiom of choice is essentially also a kind of principle motivated by the idea that an all-powerful, omniscient being could surely witness the truth of this statement, just like excluded middle. "What truths does God know?" is an interesting question to ask.
The only 'paradoxes' of choice that I am aware of are measure-theoretic ones like Vitali sets or Banach-Tarski, but these paradoxes are arguably just an artifact of basing measure theory on point-set topology rather than locales.
