There is a strong correspondence between mathematics and
programming, under which mathematical proofs correspond to
programs. A *proof assistant* is a tool that a
mathematician/programmer can use to represent proofs/programs, in
such a way that a computer can verify whether or not they are
correct. The use of proof assistants in math and computer science is
becoming ever more important for managing the increasing complexity
of proofs and programs. Proof assistants have been used to check
significant mathematical theorems, such as the Four Color Theorem,
the Kepler conjecture, and the Feit-Thompson Odd-Order Theorem, as
well as large pieces of software, such as a C compiler and the
definition of the Standard ML programming language.

### Objectives

In this course, you will learn to
*use a proof assistant to write computer-checked programs and
proofs.* Specifically, you will use
the Agda
proof assistant to verify functional programs. More broadly, you
will improve your ability to *program and prove at the same
time*.

Prerequisites: COMP 212 (CS II), or permission of instructor.

### Activities

There will be two course meetings per week. This time will be used
for chalk-board lectures, for interactively coding as a whole class,
and for small-group or individual work. Because the material
covered in this class is cutting-edge research, there are no
comprehensive written sources, and the material that we develop
during lecture will be your primary resource. Which is to say:
attendance is strongly encouraged. In the first half of the
semester, you will complete five weekly homework assignments. In
the second half, there will be additional homeworks (possibly
2-weeks each).

### Assessment

Your grade will be based on homework assignments (90%) and class
participation (10%).