1 For Prospective Students
In CS 245E, I will offer an alternative approach to the standard CS 245 curriculum. It will not be just a regular offering with additional topics. You will use the Racket programming language to build a series of small proof assistants (collectively called Proust) that allow human interaction in order to construct automatically-verifiable proofs in propositional and predicate logic. We will discuss topics such as soundness, completeness, relationships to semantic models of truth, and connections among logic, functional programming, and type theory. We will then use the Agda proof assistant to further explore the ideas of machine-checked mathematical theorems and verified software. There are optional readings and exercises for the Coq proof assistant also.
The course is aimed at students with good mathematical aptitude and reasonable programming skills, but that describes a larger number of students than typically take "enriched" courses. My intention is to provide suitable challenge, not extreme difficulty. I believe that many of these ideas will work in a regular offering of CS 245, though I have never had the opportunity to test that theory. The textbook contains additional not-for-credit exercises and optional extra readings, in the hope that students willing to take an "enriched" course will sometimes do things that do not contribute directly to their final grade.
The official prerequisite for the course is a grade of 85% or higher in CS 136, but in fact CS 136 is almost irrelevant for this offering (and indeed for CS 245 in general). Better qualifications would be good performance in CS 135/145 and Math 135/145. This is mainly what I will consider if demand exceeds the number of spaces and I am asked to be involved in selection, but in that case I will be looking at other factors as well. If you are not permitted to indicate interest in the course via Quest, you may also directly request consent to enroll from me; please include an informal transcript, and reasons why you should be allowed into the course.
Necessary background: I will expect you to be able to program in full Racket, for which CS 136/146 should be adequate preparation (perhaps with a bit of review). We will be using some Racket features (notably pattern matching and hash tables) which are used in CS 145/146 but not CS 135/136. At points, students who took CS 145/146 may have a slight advantage in having seen some ideas before, but I will try to make sure that students who have not seen these ideas are not disadvantaged.
I won’t expect you to remember specific theorems from Math 135, but I will expect you to remember the ideas of proof that were covered there, perhaps upon being reminded by me. For those who took Math 145, you may have been expected to pick up such ideas indirectly from the material, and you may need to work a little to articulate them in your mind. Those who took Math 145 with David Jao will have used the proof assistant Coq, but in a very different way from how Proust, Agda, and Coq are used in this course.