Well, there seems to be a lot of literature. I have encountered similar questions once when discussing problems in deformation quantization. here the ordered field is simply the field of formal Laurent series $\mathbb{R}((\hbar))$ with the ordering that $\hbar$ is positive (this fixed it uniquely). The idea was to transfer as much of stuff from $C^*$-algebra theory to the formal star products which are algebras of the above non-Archimedian field. Ultimately, we wanted to develop a spectral theory for these algebras, which utterly failed :) Nevertheless, you might be interested in examples of such fields and the "completed Newton Puiseux field" might be a funny one. First you take the algebraic or real closure of the formal Laurent series yielding the Newton-Puiseux series. This is not yet complete (in the sense of convergent Cauchy sequences) so you still have to complete it. The result is again field (either real, i.e. ordered) or algebraically closed, the smallest one containing the formal Laurent series.
Let me probably clarify what I mean by completion here: since you have an ordered field, the naive $\epsilon$-definition of a Cauchy sequence makes sense with the main point that the $\epsilon$ is now a positive element of you field and not just a positive real number. So this defines a topology on your ordered field, but also a uniform structure. So one can speak about Cauchy sequences and completeness etc. It is then a standard argument to show that the completion (in the sense of uniform structures, i.e. taking Cauchy sequences module zero sequences) gives again an ordered field and the original one is included via constant sequences as usual. The slightly less trivial point is that if you start with an ordered field which is real closed then the completion is again real closed. This is needed to see that the completed Newton-Puiseux series are indeed both: real (or algebraically, in the case you started with $\mathbb{C}$ instead of $\mathbb{R}$) closed and (Cauchy) complete.
A first reading may be
Narici, N., Beckenstein, E., Bachman, G.: Functional Analysis and Valuation Theory. New York: Marcel Dekker, 1971.
However, the main point is that analysis does not work too well. The reasons is that whenever you need suprema, you're on your own. And this happens quite often in analysis :) The other problem arising is that $1/n$ is no longer a zero sequence, a fact which is also used very often in analysis: you named already the intermediate value theorem...
So my conclusion is that notions of positivity work well (needed a lot in formal DQ and representation theory of $^*$-algebras) but notions of calculus do not work well.
In line with what is actually asked in the bold part of the question, I have taken the liberty of changing the title from constructive mathematics to computation. As it stood it was essentially a duplicate of another one, which already contains a lot about constructive but non-computational mathematics and so that would be the appropriate forum for further such discussion.
In fact Valery tagged the answer to the end of his first paragraph, namely @AndrejBauer's Efficient Computation with Dedekind Reals, which describes the ideas behind his Marshall calculator, whilst being based on our Dedekind Reals in Abstract Stone Duality and my Lambda Calculus for Real Analysis.
The setting for this answer is my ASD programme. I refuse to carry the baggage of obsolete programming languages (Turing Machines and Gödel Codings), any form of set theory (CZF, which I think is the setting for Lubarsky and Rathjen's paper, or even a topos) or the two bolted together (computable analysis in Weihrauch's TTE).
Valery's definition of a Dedekind cut is correct, but (to underline my rejection of any form of set theory) I write $\delta d$ and $\upsilon u$ for the down and up predicates instead of his $q\in L$ and $q\in U$ for lower and upper sets.
The predicate $\delta d$ says that (we so far know that) $d\lt x$ where $x$ is the real number being defined and similarly $\upsilon u$ means that (we so far know that) $x\lt u$.
Where this knowledge is incomplete, the pair $(\delta,\upsilon)$ satisfies all but the last axiom (locatedness) and is equivalent to an interval.
In particular, Dedekind cuts are two-sided. Taking the complement would amount to deducing knowledge or termination from ignorance or divergence.
There are plenty of examples of limiting processes that define "uncomputable" numbers that are best thought of as one-sided cuts. For example, the domain of definition of the solution of a differential equation is something that is only known from the inside; it is remarkable if we can obtain some knowledge from the outside, not that the boundary is "uncomputable" in this sense.
In the case where the cut defines a rational number, it should occur on neither side (Dedekind's choice was wrong here).
Defining the usual stuff in elementary real analysis is much easier and more natural using Dedekind cuts than with Cauchy sequences. Consider Riemann integration: $\delta d$ holds if there is some polygon (piecewise linear function) that lies below the curve and has area more than $d$; deducing the various properties from this is easy. This is gratuitously difficult if you insist in advance that the polygon have a particular shape of resolution $2^{-n}$ to make a Cauchy sequence.
The essential difference between a Dedekind cut and a Cauchy sequence as the representation of the solution of a mathematical problem is that Cauchy assumes that the problem has already been solved (to each degree of precision), whereas Dedekind merely combines all the formulae ("compiles" them into an "intermediate code", if you like), so that the problem remains to be solved.
This means that deriving a Cauchy sequence or decimal expansion from a Dedekind cut in general is just as difficult as solving a general real-valued mathematical problem. So I am under no illusion about the difficulty in implementing this proposal.
But it is a novel and so valuable way of looking at things.
The predicates define open subspaces of $\mathbb R$, so I would think that, in terms of recursion, they have to be $\Sigma^0_1$ or recursively enumerable. (I have thought a little bit about "descriptive set theory" (a name that needs to be changed) but haven't got very far with it.)
These predicates $\delta$ and $\upsilon$ are in the language of ASD and you will need to read the papers that I have linked to find out the details.
In the first instance, such predicates are built from $f(\vec x)\lt g(\vec x)$, where $f$ and $g$ are polynomials, using $\land$, $\lor$, $\exists$, recusion over $\mathbb N$ and universal quantification over closed bounded intervals.
We are given that $\delta d$ and $\upsilon u$ hold for certain rationals $d$ and $u$ and want to find some $d\lt m\lt u$ that is nearer to the result and whether $\delta m$ or $\upsilon m$.
In the case of $f(\vec x)\lt g(\vec x)$ we can use the (formal, interval) derivatives of $f$ and $g$ and the Newton--Raphson algorithm to do this. As is well known, this algorithm doubles the number of bits of precision at each step. This would justify the claim that the computation is efficient if we can extend it to more general formulae.
For more complicated logical expressions, Andrej developed a method of approximating these expressions with simpler ones. See his paper for details of this. This is quite closely analogous to methods of approximating real-valued functions by low(er) degree polynomials that have a very long history but have been developed in interval computation by Michal Konecny. Whilst Michal himself has used these computationally, they have not yet been incorporated into Andrej's calculator, but I hope that this will be done in future.
Computations like this with so-called "exact real arithmetic" are necessarily non-deterministic with regard to the Cauchy sequences tat they produce, which means that the existence of the completed sequence necessarily relies on Dependent Choice. This is entirely natural from a computational point of view and I don't see what use there is in discussing it as an issue of constructivity.
Best Answer
In the topos of sheaves over $\mathbb{R}$ we can construct a sub-ordered field of the Dedekind reals that does not have meets and joins. We recall that we can explicitly describe the Dedekind reals in $\mathrm{Sh}(\mathbb{R})$ as the sheaf $R$ where $R(U)$ is the set of continuous functions $U \to \mathbb{R}$. We define $R'(U) \subseteq R(U)$ to be the set of differentiable functions. We need to check that $R'$ is a sheaf. However, we can show this directly since differentiability is a "local" property: if $(V_i)_{i \in I}$ is an open cover of $U$ then $f : U \to \mathbb{R}$ is differentiable iff its restriction to every $V_i$ is.
We make $R'$ an ordered field by restricting the ordering and field operations of $R$. In particular, note that differentiable functions are closed under addition and multiplication, include the constantly 0 and constantly 1 functions, and that if $f : U \to \mathbb{R}$ is such that $f(x) > 0$ for all $x \in U$, then $1 / f$ is differentiable.
Since $R'$ is a sub ordered field of $R$ it inherits several properties. In particular, it is Archimedean and connected.
However, $R'$ does not have meets and joins. E.g. the zero function and the identity function do not have a join. For any differentiable function $f$ such that $f(x) \geq 0$ and $f(x) \geq x$ there is another differentiable function $g$ with the same property but strictly smaller than $f$ on some inhabited open set.