The long road from ideas to bits and back: a traveller's guide to verifiable computational research

Add to your list(s) Download to your calendar using vCal

• Konrad Hinsen
• Tuesday 21 March 2017, 13:30-14:30
• FW26.

If you have a question about this talk, please contact Matthew Danish.

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?

This talk is part of the Testing & Verification For Computational Science series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Testing & Verification For Computational Science
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.