Dear Andrej, wasn't aware of the fact that insisting on fixed rate of convergence can make things slower. My argument BTW was not about speed but rather about the ability to read off the desired result. In case of Cauchy sequences I need the modulus of convergence to know when I am close enough. In case of Dedekind reals that's not needed PROVIDED the left and the right set are given by enumerations of rationals. I "just" have to wait till close enough approximations from left and right have been enumerated. But is it right that in your implementation the left and right cuts are given by ENUMERATIONS of its elements and now via semidecision procedures? I guess so. Well, but when considering Dedekind cuts this way it essentially boils down to introducing reals as interval nestings (as done in High School sometimes). So really the question is whether Cauchy sequences or interval nestings are better. The way I interpret your remarks is that interval nesting is better since it allows one to avoid moduli of continuity which is good since fixed rate of convergence is a source of inefficiency. I think even constructivists refuting impredicativity have no problem to embrace representations by interval nestings. If I am not mistaken one finds this also in Martin-Loef's 1970 book. Thomas