ZFC implies that the reals have a well ordering, but this well ordering is, in some sense, provably uncomputable.

Given some facts about isomorphisms between well-orderings with base sets of the same cardinality, could one not prove that a well ordering of the reals is equivalent to something in an extremely non-constructive way?

And given that you tagged this question "math-philosophy" I feel I should point out that intuitionists like Brouwer would have answered the original question with a resounding NO!