The fun and honestly quite revealing part of the course was that operations on matrices even if applied using higher level primitives of conformal partitioning, the same techniques one uses for proving matrix properties could yield fast routines.

A side effect was these primitives used as a DSL not only generated fast C code but also generated a human believable proof of correctness (as opposed to automated theorem proving) rendered in LaTex.

Anyone who likes this style should also checkout PLAPACK [1].

Both FLAME and PLAPACK are by the same author.

[0] https://www.cs.utexas.edu/~flame/pubs/fire.pdf

[1] https://www.cs.utexas.edu/~plapack/