Have you ever been frustrated after spending hours trying to debug
a program, but didn't know what the problem was?
Have you struggled with putting together a proof for a theory
class, but didn't know what needs to be said, how it is supposed
to come together, or if you made some obscure mistake?
Do you wish your computer could help you fix these problems,
instead of causing more of them?
Logic, Programs & Verification is about the
proofs-as-programs paradigm, where you can learn the
tools that can give you confidence that your programs do what you
want, as well as instructing your computer to make mathematical
proofs for you. By the end of the semester, you will know how to
use formal methods to specify what programs should do, implement
software based on that specification, and verify that your code is
correct.
This course will include an introduction to different systems of
formal logic and their connection to programming languages. We
will use the relationship between proofs and programs to describe
the desired behavior of code in a way a computer can understand,
and use formal methods to write machine-checked proofs of
correctness.
On the practical side, this course will offer hands-on experience
with software tools known as proof assistants —
specifically Coq — to
write programs and proofs at the same time. For exercises, we
will use the
textbook Software
Foundations that provides both working examples and practice
problems. Students will have time to work on these exercises and
get feedback and assistance from the instructor during an in-class
lab session (in the second half of the posted class time)
following lecture.