> The approaches using equivalence classes of Cauchy sequences ... suffer from an inability to identify when two “real numbers” are the same
Perhaps there's no computable general method, but it seems like it highlights an even bigger problem which remained unspoken. There is an inability to tell when a sequence of numbers approaches zero!
Yup, you can define distinctness of constructive real numbers as two algorithms returning rationals that will differ by more than the approximation error ε they were given as input, for some arbitrarily small ε - but equality involves proving that two algorithms will never be apart in this way - and this cannot be done in general. As you say, even comparison with zero is problematic. So instead of equivalence relations, you need to define the apartness relation - the notion that a supposed equivalence between two such numerical algorithms can be constructively refuted. This is nothing new - it's a well-known part of constructive math, and is also the sensible way to formalize numerical analysis.
> The approaches using equivalence classes of Cauchy sequences ... suffer from an inability to identify when two “real numbers” are the same
Perhaps there's no computable general method, but it seems like it highlights an even bigger problem which remained unspoken. There is an inability to tell when a sequence of numbers approaches zero!