AlexFest: Dave Musser - Programming Proofs

David Musser - https://en.wikipedia.org/wiki/David_M... is one of Alex’s earliest and longest collaborators. Their work together on generic programming libraries for Ada was the precursor to the C++ STL https://en.wikipedia.org/wiki/Standar..., and he contributed ideas, algorithms, and code into the early STL. In this talk, David shows some of Alex's favorite algorithms, greatest common divisor (a.k.a. greatest common measure) and fast exponentiation along with proofs expressed in the Athena proof development system.