<jats:p>We propose a simple imperative programming language, ERC, that features
arbitrary real numbers as primitive data type, exactly. Equipped with a
denotational semantics, ERC provides a formal programming language-theoretic
foundation to the algorithmic processing of real numbers. In order to capture
multi-valuedness, which is well-known to be essential to real number
computation, we use a Plotkin powerdomain and make our programming language
semantics computable and complete: all and only real functions computable in
computable analysis can be realized in ERC. The base programming language
supports real arithmetic as well as implicit limits; expansions support
additional primitive operations (such as a user-defined exponential function).
By restricting integers to Presburger arithmetic and real coercion to the
`precision' embedding $\mathbb{Z}\ni p\mapsto 2^p\in\mathbb{R}$, we arrive at a
first-order theory which we prove to be decidable and model-complete. Based on
said logic as specification language for preconditions and postconditions, we
extend Hoare logic to a sound (w.r.t. the denotational semantics) and
expressive system for deriving correct total correctness specifications.
Various examples demonstrate the practicality and convenience of our language
and the extended Hoare logic.</jats:p>