Scale By the Bay 2021 intro video by Ryan Orendorff
Recording: Scale By the Bay 2021 intro video by Ryan Orendorff
[Music] hi my name is ryan orendorf and i will be given the talk functional programming plus dependent types is equivalent to verified linear algebra linear algebra is the backbone of many critical applications such as machine learning modern tooling makes it easy to program with linear algebra but the resulting code is prone to bugs from indexing errors improperly defined matrices and other problems that arise only when the code is executed in this talk we will seek to prevent these bugs at compile time by formalizing basic linear algebra operations in agda to do so we will represent a matrix as a function from one vector space to another this matrix-free construction will enable us to prove basic properties about linear algebra and this representation has the added benefit of being performant in terms of both space and compute time when applied in practice we will extend this concept to demonstrate implementations of matrix-free optimization algorithms that are correct by construction meaning that we can prove our function based implementation matches the matrix based implementation finally we will compare our active framework with similar matrix-free frameworks written in python and independently typed haskell to illustrate the trade-offs when adding more and more formalism to the matrix free concept