243 – Formal Specification and Proof
Guest: Benjamin Pierce Host: Markus Voelter Shownoter: Bastian Hundt
The increasing complexity of software requires increasingly sophisticated means of ensuring its correctness — “just” testing is not necessarily good enough, depending on the domain in which the software is used. Formal specification, verification and proof is a field with a long tradition in computer science that is gaining more (practical) relevance these days; and in this episode, we cover the basics. Our guest is Benjamin Pierce, professor of computer science at UPenn. We discuss the nature of (good) specifications, how verification and proof is different from testing, and where and how these techniques are successfully used today.
For further details, you might want to check out Benjamin’s (free online) book Software Foundations.
Introduction of Benjamin C. Pierce00:02:14
Intro to the topic00:03:09
Critical infrastructure | Complexity | Modular programming | Compiler | C programming language | C++ programming language | Buffer overflow | Correctness | Semantics | Unit-Testing | Formal specification | Test coverage
Other uses of Formal Specifications01:05:14
Testing vs. Proofs01:16:19