The absence of excessive numerical rounding errors is a requirement for correctness in many areas of scientific computing. Unfortunately, most high-performance computing modules lack specifications for their accuracy and stability. Additionally, few automated tools are available to scientific software developers for helping to ensure that programs produce acceptable roundoff errors for their particular application. This leaves scientific software in a precarious position, especially as software must adapt to computing environments with reduced precision arithmetic.
In this talk, we propose a type-based solution to the problem of developing accurate and correct numerical software. We will introduce a novel functional programming language called Numerical Fuzz, featuring a type system that can express quantitative bounds on roundoff errors. Our type system combines sensitivity analysis, enforced through a linear typing discipline, with an effect system for modeling rounding modes. This approach tracks the accumulation of roundoff errors and restricts the use of inaccurate programs.
