Paul has asked why most constructivists have a preference for Cauchy numerals. Well, most constructivists haven't since under the widely accepted AC_N they coincide. This, of course, doesn't deny the fact that in many sheaf toposes AC_n fails. But from point of view of the BHK interpretation AC_N is most natural. But I think the reason for prefering Cauchy over Dedekind has a quite pragmatic reason. What you are interested in is a Cauchy sequence of reals with a fixed rate of convergence (ensuring e.g. that the n-th item has distance < 2^{-n} to the limit). AC_N of course allows you to magically find a modulus of convergence for every Cauchy sequence. But like Church's Thesis or Brouwer's Theorem this is sort of a Deus ex machina (actually those are 2 contradictory dei ex machina!) and thus of moderate help for exact computation on the reals. If you base your reals on Dedekind's idea you may certainly compute with them but the result isn't very telling because a computable Dedkind real is a semidecision procedure telling you whether a given rational interval contains the (ideal) real under consideration. This doesn't help you at all to compute the real up to a given precision because you have to first guess the right interval. Of course, you may consider a partition of some area of guesses and apply the semidecision procedure to all those intervals in parallel. But that's very inefficient and can't be implemented within usual sequential programming languages. Thomas