This talk introduces a simple imperative programming language supporting real number computation that can model core fragments of existing imperative exact real number computation software (e.g., iRRAM). We design its sound precondition-postcondition-style verification calculus that can be used to prove various exact real computation programs. Finally, we extend this framework rigorously with other continuous objects such as complex numbers, sequences, matrices, functions, and so on. We also take a quick look at some recent progress on exact real computation program extraction from proofs based on axiomatic real numbers. This approach enables us to achieve verified programs in exact real computation software that are functional such as AERN.