Abstract

The translation of a scientific question into bit patterns in a computer’s memory involves many steps, as does the back-translation of the results of a computation into scientific insight. Each step is a potential source of mistakes, and thus requires some form of verification before we can trust its correctness. In this talk, I will outline appropriate verification approaches for each step, which range from purely human efforts, in particular the critical inspection of formulas and program source code, to fully mechanical procedures such as type or unit checking. I will also adopt a long-term perspective, focusing on the tools, procedures, and teaching curricula that we ought to develop in order to establish a trustworthy verification chain for computational science, even if they require a change of habits compared to today’s state of the art. In particular, I will argue for the necessity to develop digital scientific notations as the main human-computer interface of computer-aided research.

In the course of this discussion, I will also try to shed some light on a few long-standing mysteries in computational science: Why is testing floating-point code so difficult? Why is it so hard to make scientific computations reproducible? Why is there less use of static type checking in science, despite it being considered evidently beneficial in computer science? Why do we trust computations uncritically, even though we witness the unreliability of computing technology in daily life?