In this episode I discuss the amazing idea of doing mathematical proofs about our software, and contrast it to other methods for ensuring code quality, like testing or code reviews.  I also start talking about Agda, in particular some of the differences we will see from coding in Haskell, despite a lot of connections between Agda and Haskell.