Re: Dedekind versus Cauchy reals

[Vaughan Pratt <pratt@cs.stanford.edu>]

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