Collaborative Course Construction and Feedback

We are together in unprecedented times. The typical course structure implicitly assumes regular whole-class in-person meetings. We will not have that this semester. No student will be physically present in class on all days. Some students may not be physically present in class at all, or on campus period. This change affects much of the course infrastructure. As such, I want you all’s feedback and input. I am open to suggestions and changes; I consider this preliminary until the end of the first week of class. You can see any and all changes on the course website’s repository.

I cannot promise that we will act on all suggestions, and even those we find compelling may not be implementable as we go.

Purpose and Objectives

CS 2800 will introduce you to formal logic and its deep connections to computing. The goal of the course is to introduce fundamental, foundational methods for modeling, designing and reasoning about computation. This course considers approaches to proving programs properties including termination, correctness, and safety. The course also introduces students to modeling with logic the range of artifacts and phenomena that arise in computer and information science.

After this course you will know how to:

  1. translate statements about programs’ behavior into logical claims
  2. prove such claims both by hand and via automated tools.

After this course you will appreciate the benefits thinking logically when developing software, as well as the benefit of formal tools for ensuring software correctness. You will also familiarize yourself with

  • propositional and first order predicate logic
  • logical inference
  • mathematical and structural induction
  • recursion
  • equational reasoning,
  • rewriting, and
  • various proof techniques

as well as the common notations for the preceding. We will study logic from a computational perspective using the ACL2 Sedan theorem proving system. Please do not use the installation instructions on the this website. Instead follow the first lab assignment.

Contact

The best way to get in contact for personal, private (FERPA, etc) messages is via my email address jhemann@northeastern.edu. You should expect a response within 48 hours. You will find that I am faster with Piazza or our public forums. If I deem it even potentially useful to others, I will likely anonymize your letter, re-post it on Piazza, answer it there, and forward you the link.

A great regular way to reach out for help is via our office hours.

Final Exam

We will not have a final exam. Instead, our course will have a final project component. During finals week, we will schedule slots for students to present their final projects.

Grade Breakdown

I will assign overall course grades as follows:

 | Category                  | Weight (%) |
 |---------------------------+------------|
 | Lecture, Quizzes          |         10 |
 | Homework                  |         30 |
 | Lab                       |         10 |
 | 1st Project Proposal      |          5 |
 | 1st Project               |         15 |
 | Final Project Proposal    |         10 |
 | Final Project             |         20 |
 | Total                     |        100 |

We (I) will calculate overall numeric grade according to this grading scheme. Your final grades will be at least as good as the standard calculation for As, Bs, Cs, etc. To assign final letter grades at the end of the term I sum and chart the numeric scores, and break students’ grades where we see inflection points (with no students’ grade worse than their raw calculation). This means I cannot give you a more precise estimate of your grade than what you calculate from the raw score.

I will base some portions of your lab, homework, and lecture quiz grades on completion and submission of the relevant exercises. I will base the remaining portion of each on correctness.

Lab Assignments

We will expect your presence and participation in Lab. Often our lab exercises will help set you up for homework, and lab sections will solve them together. We will grade some lab assignments on completion, some on correctness, and some on one part vs. another (i.e “spot checking”). You should at least try to do some of this wholly on your own. It’s good to have a baseline early on to know if you have this material under your belt or if you are getting lost. We will not accept any late submissions except under the most dire of circumstances (family emergencies, hospitalizations, the like). We will drop the lowest lab grade; this serves as the clemency policy for late work as well.

Total Running Grade Calculation

We will track the completion portions of your lab and homework grades, as well as your project grades, in handins. We will maintain a record of the remaining grades, and will update you with the current status of that before the drop deadline (For future terms, I will change this to the Add/Drop deadline). Please ignore the grade tracker on Canvas and the handins server. We cannot give you a standing completion percentage of your quizzes and correctness grades because, logically, there are no pop quizzes.

Participation

I expect you to attend lecture and lab each class period. Your attendance is a prerequisite for a substantial portion of the course’s grade. We will not take attendance as such, but the following proxies serve as an attendance grade:

Reading, Content Quizzes

Before class, I will expect you to have read the notes as marked on the schedule. There may be quick pop quizzes during the session. These act as a forcing function for the lecture notes and alert me to students’ difficulties. Sometimes we take these for completion, others for accuracy. These grade belongs under “Lecture Quizzes.”

Homework Submissions

Unless otherwise indicated, homework submissions are due by 10pm on the Monday after I have assigned them. To universally, uniformly and preemptively account for any number of situations that arise, I will drop every student’s lowest homework assignment grade. This absolution for one assignment is our late/etc homework clemency; I shall not accept late homework otherwise; we are, however happy to go over your submissions with you at office hours. Unless otherwise indicated, you should work on homework in the team you have selected on handins.

Oral Homework Explanations

Proof has a social component. As such, part of your homework grade will also include your ability to communicate the meaning of your proof to your colleagues. You will be randomly selected from the class roster to walk us all through some answer of yours. Being absent from class means you cannot participate. Not all homework questions will get an oral explanation. To explain other homework questions’ answers we will ask more than one student to trade off. Some others questions we will take for completion or grade ourselves for accuracy. Regardless these grade belongs under “Homework” as well.

TRACE evaluations

I encourage students to take time and submit TRACE evaluations. Your time is busy at the end of the term when these are available. In order to fairly compensate you for that time, if 85% or more of the enrolled students complete these TRACE evaluations, then I shall add 2 points onto the class-wide final average.

Recent Changes

This semester we will leverage more project-based assignments, including individually or group-selected proofs for topics that have come up in practice. Students will complete two of these, a small one and a big one. The former also serves as practice for the latter.

I’m also planning to use some of the last part of the course, while students are working on these larger projects, to talk about computational logic in a different context: logic programming. We can also get into the “guts” of an implementation of such a system, where ACL2, ACL2s is so much more sophisticated that it’s tough for students to wrap their heads around an implementation.

If in fact you’re interested in PL research, logic, logic program, automated theorem proving or the like, please let me know on that too! I’m excited to talk more about it all :-)

Projects

We have two projects in this course. Together with your partner/mob, you should start thinking about something worth proving. These might come from Fundies I, Fundies II, from your math classes, or somewhere else from your own experience. These should be large enough to be of interest and challenging. The proof should be in some way enlightening.

First Project

I will grade the first of these projects “more easily” than I would otherwise have done so. I will ensure this by fitting grades to a roughly normal distribution with a median no lower than a B+ average. I will for this first project also grade more lightly on grammar where it does not seriously impede my understanding. You should schedule a slot for your pair/mob to present here.

Second Project

Based both on feedback and experience I have revised how I manage and execute the second of these projects. I release the project guidelines approximately one month before its due date. When I do so you will have also a timeline outlining your due dates for each stage. You should expect the following stages:

  • Roughly four days to one week after I’ve assigned your second project, your group will meet with me virtually to discuss your project idea and get clearance to proceed.

  • Roughly two weeks before its due date, you will submit to me a progress report with source code and your status at this point.

  • Roughly two to four days before the due date, you will have submitted to me a “receipt” for an appointment at the writing center where you have copy-edited your draft. They have a whole bevy of resources for you.

  • Roughly a month after I’ve assigned your second project, your group will submit to me via a Dropbox your project report, either:
    1. as a zip archive containing your PDF and your source code, with suitable instructions for me to build and run your deliverable.
    2. If your document contains a link to a source repository that I can access, you may simply submit a stand-alone PDF.
  • Roughly a 28 to 34 days after I’ve assigned your second project, your group will meet with me virtually to discuss and demonstrate your project and results.

Academic Integrity Policy

Students of course play an integral part in ensuring they receive the full benefit of their coursework. The students of 2800 are certainly beholden to the academic integrity policies of Northeastern University, the Khoury College.

Teamwork and Collaboration

Pair programming is a central part of the undergraduate curriculum here. Pair programming is not intended to divide-and-conquer, but instead for students to collaboratively solve problems together. You are only twice as fast working separately if the typing is by and away the hardest part of programming. Which it is not.

Ultimately, you should be responsible for and have a firm understanding of all work submitted under your name. You should be able to demonstrate this mastery when requested.

Required Texts

There are no required texts for this course. Our course will follow a draft of Pete Manolios’s /Reasoning About Programs/ (2020). You will find these notes linked from this website. I invite you to collaboratively annotate these notes with me, and with each other.

Academic Accommodations

If you have accommodations from the Disability Resource Center (DRC) please submit your Professor Notification Letter to me by email, preferably within the first two weeks of the quarter, so I can do my part to help you achieve equal access in this course. I am eager to discuss ways we can ensure your full participation.

I encourage all students who may benefit from learning more about DRC services to contact the DRC.

Technology and Platforms

As a course and a student body, we are more remote than usual, and preferable. We will leverage a number of Northeastern’s technology platforms to help bridge the chasm. Your first lab assignment will walk you through installing and configuring these.

We will use a variety of tools and platforms to facilitate teaching and learning at a somewhat remote distance and to compensate for this unconventional semester. These include ACL2s, Eclipse, VirtualBox, CodeTogether, WaitWhile, PollEverywhere, and Hypothes.is. Please see the technology page for more details.

Health and Safety

The university has put into place a robust plan to make the campus healthy and safe for all — but you must do your part. On August 22, all students received an email from Senior Vice Chancellor for Student Affairs Madeleine Estabrook on the expectations for behavior both on campus and off campus. Please read it carefully today.

To summarize:

  • Gatherings on or off campus must conform to healthy practices as outlined by university and Massachusetts state guidance. If you host or attend an inappropriate party or gathering, you run the very real risk of immediate removal from the community.

  • Wear a mask indoors and outdoors as you maintain a 6-foot distance from everyone.

  • Get tested every three days using the COVID-19 Test Scheduler (covid19-testing.northeastern.edu.) We may require more frequent testing as the semester progresses. It’s quick, easy and will help us to quickly identify and care for anyone who tests positive. I will not be told the identity of anyone who tests positive, and you do not need to share that information with me or anyone else unless you want to. If you receive a positive test result, you will be contacted by a member of the university’s telehealth team who will provide you with next steps.

  • Do a Daily Wellness Check (wellness-check.northeastern.edu), wash your hands well and regularly, and disinfect high-touch surfaces and spaces.

  • I will be wearing a face covering or mask as I teach and expect that you will do the same in class. If you come to class without a mask, I’ll ask you to go and get one on campus. You can get a mask at the Visitor Center or at the Curry Student Center Help Desk. If you refuse to wear a mask in class, I won’t be able to continue the class. If you are not sitting six feet apart from your classmate, I’ll ask you to do so. We won’t be able to eat or drink in class (except water). If you test positive, you will need to enter isolation as directed by the university’s telehealth team. I expect that you will not come in-person to class and that you will follow the guidance from the university telehealth team to isolate and get appropriate healthcare if needed.

  • Staying safe is a responsibility that we all must take seriously. Keep in mind the “Protect the Pack” theme. Remember that our individual actions will help everyone stay safe this fall.”

Acknowledgments

Pete Manolios is responsible for much of our course infrastructure and assignments. Pete Manolios and Stavros Tripakis inspired some the lecture contents and topics, and in some cases designed the slides. Lindsey Kuper inspires some of this site as well as being all-around inspirational.

In the syllabus