Formal Reasoning about Software

In this course, we learn the fundamentals of formal reasoning about programs. The basis for reasoning is logic, specifically, propositional and predicate logic. Within logic, we formally specify programming languages, that is, their syntax and operational semantics. We also formulate specifications of programs and prove that given programs satisfy their specification. The logic we work in is itself implemented as a computer program, in a so-called computer proof assistant. We learn how to implement our logical reasoning in a computer proof assistant; the activity of "proving" thus becomes a form of programming itself.