The use of the axiom of choice can often be avoided by working directly with algebraic/ observational objects. As an illustration of a general elimination theorem we present a constructive and elementary proof of the Stone-Yosida representation theorem for Riesz spaces (vector lattices). This proof is motivated by considerations from pointless topology. This theorem implies the famous Gelfand representation theorem for C*-algebras of operators on Hilbert spaces.
This will also be put in a more general context of proof mining and the implementation of infinite objects in computer algebra.