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
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 and imperative programs, and
to formalize mathematics
in Homotopy Type
Theory. More broadly, on the computer science side, you will
improve your ability to *reason about your code*. On the
math side, you will learn how to *do mathematics based on type
theory instead of set theory*, and you will understand the
advantages and challenges of this approach.

Prerequisites: COMP 212 (CS II), or permission of instructor.
Students without knowledge of functional programming (as is often taught in CS II)
or programming languages (as in COMP 321) may need to do some extra
background reading.

### 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,
followed by a take-home exam. In the second half, there will be
additional homeworks (possibly 2-weeks each), and a final project.

### Assessment

Your grade will be based on homework assignments (50%),
a week-long take-home midterm (20%), a final project (20%),
and class participation (10%). (Percentages are subject to change
depending on the exact composition of assignments in the second half
of the semester.)