The world's shortest correct exact real arithmetic program? (Q714620)

The difference between double precision floating point and exact real number computation is well described on the fourth page of the paper. When computing \texttt{sin(1e200*pi)}, the former results in a value near 1, whereas the latter gives correctly the exact result of 0. Exact real number arithmetic is difficult, algorithms are often more subtle than their traditional counterparts and not always studied to the same extent. The application of formal methods in exact real number computation puts the reliability of these algorithms on a new level. In this paper the author presents what is supposed to be the world's shortest correct exact real arithmetic program. Correct means here concretely that the program is verified using the PVS system. The choice of system is discussed comparing it to Coq and Isabelle/HOL. PVS is used mainly since it contains libraries related to the work and since it is a non-constructive system. In further sections the representation of exact real numbers is presented, then issues are discussed of how to compute sin, cos, and log as Taylor series (after the functions are transformed so that the arguments are moved into an area where these series converge fast). The PVS proof consists of 500 theorems and over 60000 lines of code. The appendix contains in three pages the verified Haskell program.