There is an implementation of exact real arithmetic that has been verified in in Coq[1] and also an implementation in Haskell[2] which may or may not do what y

There is an implementation of exact real arithmetic that has been verified in in Coq[1] and also an implementation in Haskell[2] which may or may not do what you want to do. It really does depend on what you want to compute. For instance, I can provide a simple implementation in Haskell that includes addition, multiplication and square roots: data Real = Real add :: Real -> Real -> Real add _ _ = Real multiply :: Real -> Real -> Real multiply _ _ = Real squareRoot :: Real -> Real -> Real squareRoot _ _ = Real zero :: Real zero = Real one :: Real one = Real but it isn't very interesting as you can't print things or test for equality...Any implementation of real numbers that includes those is going to be much harder[3]. [1]http://videolectures.net/aug09_spitters_oconnor_cvia/ http://videolectures.net/aug09_spitters_oconnor_cvia/ [2]http://www.haskell.org/haskellwiki/Exact_real_arithmetic http://www.haskell.org/haskellwiki/Exact_real_arithmetic [3]http://en.wikipedia.org/wiki/Tarskis_undefinability_theorem http://en.wikipedia.org/wiki/Tarskis_undefinability_theorem