The implementation of real numbers using floats is known to be error prone. Exact real arithmetic allows one to move the burden of correctness from the user to the computer program. The correctness of this computer implementation has to be checked only once. For maximal certainty one uses a computer to check the correctness of this implementation. We illustrate how to prove correctness by implementing the Riemann integral in constructive mathematics based on type theory. The implementation and its correctness proof were driven by an algebraic/categorical treatment of the Riemann integral which is of independent interest.

This work builds on O'Connor's implementation of exact real arithmetic. An demo session will be included.