Andrej Bauer wrote:
There is no need to think of a Dedekind real as a clumsy semidecision procedure. Instead, the left and the right cut may be seen as instructions for calculating better approximations from existing ones. This can be done quite efficiently with Newton's method (the variant for interval arithmetic). The computation that comes out then behaves very much like an iterative procedure for computing a Cauchy sequence.
If everything can be related to interval arithmetic in one way or another, why not take interval arithmetic itself as the gold standard for the constructive reals? The Edalat-Escardo-Potter domain-theoretic analysis of interval arithmetic struck me as sufficiently canonical that I don't understand why all the alternatives aren't being evaluated relative to that one. Are there alternatives that compensate for some shortcoming of interval arithmetic as understood through the lens of domain theory? Vaughan Pratt