As others have mentioned, there are many different variations in the exact notion of Cauchy reals and Dedekind reals which affect the answer.

I will choose variations so that I can offer a counterpoint to Paul Taylor's claim that Dedekind cuts represent a problem that "remains to be solved." If one uses the propositions-as-types correspondence to encode Dedekind cuts as "predicative subsets" $L, U : \mathbb{Q} \to \mathcal{U}$, where, $\mathcal{U}$ is the universe of types, and also reinterprets the rules of Dedekind cuts using propositions-as-types, for instance

 - inhabitedness: $\sum_{x : \mathbb{Q}} x \in L$ and $\sum_{x : \mathbb{Q}} x \in U$

 - locatedness: $\prod_{q, r : \mathbb{Q}} q < r \to (q \in L) + (r \in U)$

then Dedekind cuts *do* represent problems which have already been solved as well. In particular, the inhabitnedess and locatedness proofs above give the computational content. By inhabitedness, one can determine that a real number lies within some finite open interval. Then, by repeatedly using locatedness to cover this interval with several smaller ones, one can narrow down the interval where the real number must be to an arbitrarily small width.

Conversely, we can put the Cauchy definition on the same footing as the Dedekind definition by treating it as a "metric completion" in the sense of [Steve Vickers's *Localic completion of generalized metric spaces I*](http://www.cs.bham.ac.uk/~sjv/loccompAA.pdf). In this framework, a Cauchy real is a predicate $B : \mathbb{Q} \times \mathbb{Q}^+ \to \mathcal{U}$ on "formal balls", where $B(q, \varepsilon)$ holds if the real number is (strictly) within $\varepsilon$ from $q$. Then one of the rules which $B$ must satisfy is
$$\prod_{\varepsilon : \mathbb{Q}^+} \sum_{q : \mathbb{Q}} B(q, \varepsilon),$$
which says topologically that for arbitrarily small $\varepsilon$, $\mathbb{R}$ is covered by balls with rational centers and radius $\varepsilon$, and *computationally*, that we can compute some $q$ within $\varepsilon$ of the real number.

The axioms defining valid Dedekind cuts as well as valid Cauchy predicates on formal balls provide a computational interface for computing with real numbers. The axioms also have a particular "geometric" form, which Vickers explains, and each suffices to define a topological space (or, more accurately, a space within the framework of locale theory or formal topology). Vickers proves (Theorem 26) that these two spaces, the order-theoretic (Dedekind) and metric (Cauchy), are homeomorphic, meaning that it is possible to use one computational interface to implement the other.

In general, the points of spaces formulated in this way may not be sets (predicatively), since one can vary the universe level of the predicative subsets. But $\mathbb{R}$ is in fact small (see [Palmgren's *Predicativity problems in point-free topology*](http://www2.math.uu.se/~palmgren/lc03proc_rev2.ps)), so in fact the points of $\mathbb{R}$ form a set.

In terms of efficiency, one would probably consider metric API more "efficient", since approximating to a rational with a tolerance of $\varepsilon$ requires 1 "API call", whereas one needs a variable number of uses of the "locatedness" rule for Dededkind cuts, and each additional call provides only one more bit of information.