In computer-aided mathematical proofs, a basic, yet critical, building block is the problem of actually obtaining numerical values. In practice, one strives to achieve precise and/or guaranteed results without compromising efficiency. For this, we combine symbolic and numerical computation, which leads to the development of specific new arithmetic and approximation algorithms. Hereof, some of these techniques are overviewed, with examples related to the efficient finite precision evaluation of numerical functions (some of which appear in practical space mission analysis and design).