Searching for Edsger Dijkstra

Robert van der Geijn and Maggie Myers
Institute for Computational Engineering and Sciences,
The University of Texas at Austin
 
will give a lecture:  
Searching for Edsger Dijkstra

in the Mathematics of Complex Systems Seminar of the Mathematical Institute, Utrecht University

date: Thursday March 15, 2018
time: 16.00-17.00
location: Hans Freudenthalgebouw, Budapestlaan 6, Utrecht, in room 611

Abstract:
"But one should not first make the program and then prove its correctness, because then the requirement of providing the proof would only increase the poor programmer’s burden. On the contrary: the programmer should let correctness proof and program grow hand in hand. “  — Edsger Dijkstra, “The Humble Programmer,” ACM Turing Lecture 1972.

One of the many contributions Dijkstra left the world was his advocacy of programming as a science rather than an art.  Mathematical tools towards this end proposed by him and some of his contemporaries were the notion of the weakest precondition, the loop invariant, proving a loop correct, and deriving a loop to be correct.  This last idea had limited practical impact over the decades because it requires loop invariants, which describe the state of variables before and after each iteration of a loop, to be determined a priori.  

About two decades ago, we stumbled upon a few insights that advanced this topic.  For the domain of dense linear algebra (DLA) operations, we developed a new notation for expressing algorithms that facilitates the systematic derivation of loop invariants and thus the systematic derivation of families of algorithms. Since DLA operations are at the core of many high-performance scientific computing applications, this has considerable impact: from the family of algorithms the one that yields high performance can be chosen.  Upon these principles, we have built a new DLA software stack as part of the Formal Linear Algebra Methods Environment (FLAME) project.

A natural question becomes how to take these insights beyond dense linear algebra.  Our approach has been to develop a Massive Open Online Course (MOOC) titled “Programming for Correctness” that is offered on the edX platform.  While that MOOC uses DLA for examples and exercises, the idea is to reach a broad audience in the hopes that researchers with expertise in domains other than DLA will extend the techniques to those domains.  Thus, the MOOC is an instrument in our search for those who can push Dijkstra’s ideas regarding formal derivation further.