That's an interesting question, but kind of hard to answer. Programming is inherently constructive so approaching a non-constructive proof as a programming problem tends to be problematic.

I don't think you run into any problems if you let the axiom of choice pick the same numbers every time. It would be a bit problematic if you were to add that as an extra axiom (suddenly every proof let x,y in X then ... therefore x=y would become trivial).