The only effective way to raise the confidence level of a program significantly is to give a convincing proof of its correctness. 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. - “The Humble Programmer,” Edsger W. Dijkstra (1972)

LAFF-On Programming for Correctness presents “goal-oriented programming” the way Edsger Dijkstra, one of UT-Austin’s most influential computer scientists, intended. The methodology demonstrates that, for a broad class of matrix operations, the development, implementation, and establishment of correctness of a program can be made systematic. Since goal-oriented programming focuses on program specifications, it often leads to clearer correct programs in less time. This approach rapidly yields a family of algorithms from which an algorithm with desirable properties, such as attaining better performance on a given architecture, can be chosen.

The free-to-audit, six-week, self-paced course “LAFF-On Programming for Correctness” launches its second offering by UTCS faculty (and spouses) Robert van de Geijn and Maggie Myers on May 15, 2018 on the edX platform. The Linear Algebra - Foundations to Frontiers (LAFF) online courses connect the theory of linear algebra to issues encountered in computer architecture, software engineering, and program correctness. The LAFF courses build on van de Geijn and Myers’ ongoing research in high-performance linear algebra libraries, exposing participants to cutting-edge research while teaching them the fundamentals of the field. More information can be found on the edX website.