Well, no, not really. The standard definition of the reals is as the unique nontrivial totally-ordered, Dedekind-complete, Archimedean field up to isomorphism.
So what you would really need is a uniqueness proof, with addition and multiplications "provided" by the hypothesis.
And how do you prove that a totally-ordered, Dedekind-complete, Archimedean field does not lead to contradiction besides constructing it explicitly by bootstrapping from natural numbers?
Nothing in the construction requires you to show an algorithm that given x, y \in R allows you to compute x+y and xy. You would make the usual Dedekind construction and show it satisfies the axioms of such a field. (as a matter of fact, no such algorithm exists in full generality!)
It's probably a tomato/tomato kind of thing, but I'm only objecting to the 'algorithm' part of parent's comment.
