3 Logistics
3.1 Textbook
The textbook will be my own Logic and Computation Intertwined (LACI), available free online, and based on the lecture summaries of my previous offerings of this course (though with much rewriting and a fair amount of new material). LACI is designed as a standalone resource for readers with some programming experience. As someone who has gone through UW’s first-year CS and Math courses, you will have some advantages over a typical reader.
I have included a number of references in the last chapter of the textbook, but not with the intention that they directly support course material. Differences in notation, meaning, definitions, assumptions, and order of coverage are likely to render most potential references more confusing than illuminating. These are best investigated after the course is over.
If you are having difficulty with course material, please contact course personnel rather than try to find something online or in the library that might help. I’m sorry to not be able to recommend any backup materials, but this is what happens when a course is a synthesis of various sources. I’m open to creating supplementary documents as needed. What I will not do is provide more examples, because I want to encourage engagement with the underlying theory. At this point in your education, and particularly in an enriched course, you should not be trying to learn based on a large corpus of examples.
3.2 Getting Help
We will be using Piazza for online public questions and discussion. If you have not gotten an invitation to the forum by the first lecture, or you join the course late, please contact me. You may also email course personnel. Please do so from your UW email address.
Office hours will be listed on the main course Web page. Office hours are not the best place to get help with partially-completed or buggy Racket or Agda code. I typically need to work with it for a while, look at Marmoset tests, and so on. The TAs may think faster than I do, but it’s likely that email is the best way to get help with code. We can see all your Marmoset submissions but if you have not submitted, attaching code to your email will help (rather than putting a snippet in the body of the email). Screenshots tend to be useless (in email, or Piazza), so think carefully about them. Proust proofs, on the other hand, are short enough that I should be able to diagnose them in real time (no promises, though).
3.3 Lectures
These will be in the style of my CS 145/146 offerings (2008-2014), with sparse slides that will not be posted, supplemented with boardwork. The difference is that in those courses, I posted detailed lecture summaries after each lecture, but now everything is available in advance, in the textbook.
I suggest taking selective notes by hand in lecture, more as a stimulus for active learning than for reference later. Consider avoiding open laptops and tablets in lecture. They are distracting to you and others, and studies show they reduce performance even when used only to take notes (which is rarely their only use in practice). Please set your cellphones on stun.
I will not in any way enforce regular lecture attendance, but I highly recommend it. Structured engagement with material is a good way to learn it. I will do my best to make lectures worth your while.
I will wear a mask while lecturing. I can’t require you to wear a mask, but I would like you to do so. Please do not attend lecture if you are sick (with COVID or anything else). It isn’t fair to the other people in the room.
3.4 Tutorials
We currently have no plans to use the tutorial slot. If we schedule anything there, it will be on optional extra topics for interest only, and announced on Piazza.
3.5 Homework
Details are available on the Assignments page. The main thing is to keep making progress so that you are not in a rush close to the end of term. I have grouped assignment questions into bundles with a weekly deadline. There is more discussion of timing on the Assignments page; I will just say here that you should consider working ahead of the schedule, since material naturally gets more challenging as the term progresses. Submission details are on the Marmoset page.
Assignment questions will primarily involve programming parts of several versions of a proof assistant (Proust) in Racket, and using those programs to develop and check proofs of theorems in a way that is itself a kind of programming. In the last part of the course there will be some programming in Agda, which is like the work that uses Proust, but with a larger scope. Different questions may have different weights. No solutions will be posted (this is longstanding policy of mine), but course personnel will be happy to help you complete questions after the due dates.
The circumstances are challenging for all of us. If you need adjustment of the deadlines, contact me in advance, with an explanation.
3.6 Grading
There is no midterm or final exam in this offering. We did without them in Fall 2020, and it was less stressful for everyone. The grade will be computed entirely as a weighted average of assignment questions. This makes it even more important that you complete all assignments by yourself, without help from online sources, books, or fellow students.
3.7 Software
You will need the latest version of Racket (8.6) and the latest version of Agda (2.6.2.2), as well as its standard library. Racket, as you know, is very easy to install. We will be using full Racket. If you are not familiar with it, you should read section 2.1 of FICS2 which is based on the transitional material I used in CS 145. We will also be using quasiquotation and pattern matching in Racket, which you can read about at the link above. There is also a similar writeup linked from section 2.5 of LACI.
Agda is used in the last third of the course. It is built on and requires the installation of Haskell, and interaction with Agda is done through the Emacs text editor. Installing Agda can be challenging, and you will need to spend some time learning how to use Emacs. There are some tips linked in the Handouts chapter of LACI. You have time for this, but don’t put it off too long.
3.8 Mental Health and Diversity
The Faculty of Mathematics has asked us to include the following material.
3.8.1 Mental Health Support
The Faculty of Math encourages students to seek out mental health support if needed.
On-campus Resources:
Campus Wellness https://uwaterloo.ca/campus-wellness/ Counselling Services: counselling.services@uwaterloo.ca / 519-888-4567 ext 32655 MATES: one-to-one peer support program offered by Federation of Students (FEDS) and Counselling Services: mates@uwaterloo.ca Health Services: located across the creek from the Student Life Centre, 519-888-4096.
Off-campus Resources:
Good2Talk (24/7): Free confidential help line for post-secondary students. Phone: 1-866-925-5454 Here 24/7: Mental Health and Crisis Service Team. Phone: 1-844-437-3247 OK2BME: set of support services for lesbian, gay, bisexual, transgender or questioning teens in Waterloo. Phone: 519-884-0000 extension 213
3.8.2 Diversity
It is our intent that students from all diverse backgrounds and perspectives be well served by this course, and that students’ learning needs be addressed both in and out of class. We recognize the immense value of the diversity in identities, perspectives, and contributions that students bring, and the benefit it has on our educational environment. Your suggestions are encouraged and appreciated. Please let us know ways to improve the effectiveness of the course for you personally or for other students or student groups. In particular:
We will gladly honour your request to address you by an alternate/preferred name or gender pronoun. Please advise us of this preference early in the semester so we may make appropriate changes to our records.
We will honour your religious holidays and celebrations. Please inform of us these at the start of the course.
We will follow AccessAbility Services guidelines and protocols on how to best support students with different learning needs.