Algorithms are certifiable, and HLF is now open
BLOG: Heidelberg Laureate Forum

As opening ceremonies go, this year’s Heidelberg Laureate Forum opening was quite enjoyable. Of course there need to be official words by representatives from key partners and supporters, such as the Baden-Württemberg Minister for Science, Research and the Arts, Theresia Bauer, university president Bernhard Eitel and Heidelberg’s mayor Eckart Würzner. But (a) those were quite entertaining, (b) HLF bundled quite a few of these into fun on-stage interviews, moderated by Master-of-Ceremonies Günter Ziegler and (c) inserted a snappy computer science talk in the middle, to liven things up a bit.

The talk, by Kurt Mehlhorn from the Max Planck Institute for Informatics, was about certifying algorithms. How do we know that software actually does what it is supposed to do? That it has made the correct calculations, found the optimal match for online dating, made the correct decision whether or not a linear system of equations can be solved?
If we were not dealing with a program, but with a human assistant, we would be asking him or her: How did you arrive at your result? Can you justify what you did? What did you actually do? Algorithm certification works in a similar way: A certifying algorithm is written in a way that it produces not only the result, but also a “certificate,” or “witness,” that is, additional information which can be used to check directly that the algorithm has obtained the correct result. A simple example: in addition to computing the greatest common divisor g of two integers, a certifying algorithm could compute, and return, two additional integers that would allow for a direct test that g is indeed the common divisor (the latter is called the extended Euclidean algorithm; this and additional examples can be found in this paper by Mehlhorn and colleagues).
Personally, I’m hoping for a Heidelberg Laureate Forum that is not only edifying, but in this specific sense, certifying: with talks and discussions that not only tell us what’s what, but provide the additional information we, the audience, need in order to decide for ourselves that what we are being told has merit.