Approximate Programming

Speaker: Eddy Westbrook 

Abstract: Real-number programs are at the core of much of computer science. Such programs are almost universally implemented using finite-precision approximations, such as fixed- or floating-point numbers, for reasons of both computability and efficiency. Approximation does not have to stop with fixed- or floating-point numbers: recent research has shown that additional approximations—such as omitting loop iterations or using less precise implementations of certain core functions—can greatly improve performance while still maintaining reasonable error bounds in many situations. A key difficulty in using approximations, however, is verifying approximated programs. This requires proving that an approximated program is quantifiably correct with respect to the original, a more complex proof obligation than traditional program correctness. In this talk, a new semantics for relating programs and their approximations is given, which can capture all of these techniques. Ongoing work on approximate program synthesis, where approximate programs and their errors are derived from real-number specifications, is also discussed.