© 2020 Strange Loop
In 1969, Tony Hoare published a paper that would change computer science forever. He reflected on the ideas of consequence in program execution and created a set of formal definitions for proving correctness. This is a far cry from how most software is verified today: through automated unit testing in the style of X-Unit. In this talk, Aaron and Daniel will brave the forgotten paths of software verification beyond the realm of unit tests. They will look at some of Hoare's original concepts and how others have built on them, gain a deeper understanding of type theory and the limitations of language-integrated proof systems, and finally examine the restrictions that can be imposed on language expressiveness to make verification more tractable.