IST Lunch Bunch

Starting in the late 1960s computer scientists, including Dijkstra and Hoare, advocated goal-oriented programming and the formal derivation of algorithms. The chief impediment to realizing this for loop-based programs was that a priori determination of loop-invariants, a prerequisite for developing loops, was not well-understood for any but the simplest of operations. Around 2000, these techniques were for the first time successfully applied to the domain of high-performance dense linear algebra libraries. This has led to a multitude of papers (mostly published in the ACM Transactions for Mathematical Software), a system for the mechanical derivation of algorithms, and a high-performance linear algebra library (libflame) that includes more than a thousand variants of algorithms for more than a hundred linear algebra operations. Key insights include a new notation for presenting algorithms for matrix computations, a "worksheet" (the weapon of math induction) that one fills out to formally derive the algorithm hand-in-hand with its proof of correctness, and APIs that allow correct algorithms to be represented as correct code without the inadvertent introduction of programming errors. Thus, years after his death, Dijkstra is having a profound and practical impact on the development of modern high-performance alternatives to widely used libraries like LAPACK and ScaLAPACK. <br><br> This work is in collaboration with the FLAME teams at UT-Austin (USA), Universidad Jaume I (Spain), and RWTH Aachen University (Germany).