The real numbers are pervasive, both in daily life, and in mathematics.
Students spend much time studying their properties. Yet computers and
programming languages generally provide only an approximation geared
towards performance, at the expense of many of the nice properties we
were taught in high school.

Although this is entirely appropriate for many applications, particularly
those that are sensitive to arithmetic performance in the usual sense,
we argue that there are others where it is a poor choice.
If arithmetic computations and result are directly exposed to human users
who are not floating point experts, floating point approximations tend to be
viewed as bugs. For applications such as calculators,
spreadsheets, and various verification tasks, the cost of
precision sacrifices is high, and the performance benefit is often not critical.
We argue that previous attempts to provide accurate and understandable
results for such applications using the recursive reals
were great steps in the right direction, but they
do not suffice. Comparing recursive reals diverges if they are equal.
In many cases, comparison of numbers, including equal ones, is both important,
particularly in simple cases, and intractable in the general case.

We propose an API for a real number type that explicitly provides decidable
equality in the easy common cases, in which it is often unnatural not to.
We describe a surprisingly compact and simple implementation in detail.
The approach relies heavily on classical number theory
results. We demonstrate the utility of such a facility in two applications:
testing floating point functions, and to implement arithmetic in
Google's Android calculator application.