Skip to content

Syllabus

Course Description

It is incredibly easy to write incorrect code. While some simple issues (e.g., returning an integer instead of a string) can be ruled out by type checking and basic testing, this can only get you so far. When other people (and your future jobs) depend on the code you write, you will need to be, in some cases, absolutely sure it's running correctly.

This course is an introduction to formal methods. For the purpose of this course, formal methods is the practice of analyzing the correctness of code via logically precise specifications and evaluating the correctness of code against their specifications. These skills are useful not only for making your code do what's indended, but also effectively communicating your code to others.

We will begin by learning about typed functional programming, which is useful for writing code that is simple, modular, and easy to reason about. After gaining this foundation, we will move on to specification: how we can turn natural language requirements of software into mathematically precise statements that can be mechanically checked. We will explore various styles of specification via a variety of programming assignments. Finally, the end of the course will introduce the main ideas of programming languages --- syntax trees, interpreters, and compilers --- with the goal of developing and deploying new ways to analyze the correctness of programs.

Learning Outcomes

Students will:

  1. Gain experience working in a statically typed functional programming language, including using their capabilities for modularity and abstraction;
  2. Learn to transcribe and invent formal specifications of programs;
  3. Gain experience in using property-based testing to evaluate the correctness of programs; and
  4. Be introduced to the basics of programming languages, including syntax trees, compilers, interpreters, and type system design.

Prerequisites

The course requires CS2500 (Fundamentals of Computer Science 1) and CS1800 (Discrete Structures). If you do not have this background, you need to get permission of the instructor.

Course Format

Website

This website will be the central location for all course information, including office hours, homeworks, and lectures.

Discord

Course communication will happen via Discord, which we will use for announcements and Q&A about the course content. While we will do our best to answer questions asked on Discord, TA office hours are a more reliable way to get immediate feedback. Use this link to join the Discord: https://discord.gg/dTcxH2RdcE.

Since messages on the Discord server are public (to course students and staff), do not share any (partial) solutions of homework on the Discord. If you have a question about your specific solution, feel free to use the Discord to request for a couse instructor / TA to send you a direct message.

NOTE: You must set your display name on the server to your full name before we give you access to the (private) course channel.

Gradescope

You will use Gradescope to submit homework assignments, and the feedback you will get will be available on Gradescope. If you go to Gradescope and log in with Northeastern credentials, you should be enrolled in the course. The Gradescope enrollment is based on Canvas, so if you just enrolled in the course, it might take a day or two to synchronize.

OCaml

The course will be taught using OCaml, a typed functional programming language used both in academia and in industry. Information for setting up OCaml can be found here.

Evaluation

You will be evaluated on the basis of: weekly homeworks, usually consisting of programming assignments; short, in-class quizzes; and two in-class exams. Your final grade will be calculated as follows: 40% homework; 20% quizzes; 20% Exam 1; and 20% Exam 2.

Final grades will then be assigned on the following scale:

Letter Grade Minimum Percentage
A 93%
A- 90%
B+ 87%
B 83%
B- 80%
C+ 77%
C 73%
C- 70%
D+ 67%
D 63%
D- 60%
F < 60%

Homework

The main way you will learn the material, other than showing up to lecture, is completing the homework. Each homework will give you the opportunity to practice the skills taught in lecture.

Homeworks can either be done solo, or in groups of two. If you choose to work with a partner, please submit as a group on Gradescope.

Quizzes and Exams

Periodically throughout the semester, we will have short (~10-15min) in-class quizzes which will serve as a ``check-in'' about your understanding of the course material. Quizzes are announced ahead of time on the schedule.

We will have two in-class exams (also displayed on the schedule).

Policies

Late Work and Makeups

Homeworks are typically due 11:59pm on Sunday, and will be released the Friday the week before. However, do not wait until the weekend to begin the homework. Think of the "real" deadline as 11:59pm on Friday, with the weekend as a grace period. There will be no late work accepted after 11:59pm. If you require a special accomodation or an extension, please email the instructor in advance of the deadline (by Wednesday the week the assignment is due, at the latest.)

Regrades

If you think a factual error was made in any graded assignment (homework, quizzes, or exams), you may submit a regrade request at most 7 days after the feedback was released. All regrade requests must make an explicit reference to a rubric item that was used incorrectly.

Collaboration

You may work with a partner on all homeworks. Do not share any code or homework solutions with anyone who is not your homework partner.

Homework will be a significant part of your learning experience. If you share solutions, you are not only violating academic integrity, but you are depriving the other person of their opportunity to learn the material.

On the other side, if you consistently rely on others to help you solve the homework, you will likely suffer in the quizzes and exams, which are a significant part of your grade.

AI Tools

You may not use any AI tool, such as an LLM (ChatGPT, Claude, etc) to aid in any assessed material, including homework. The role of CS2800 is to teach you how to reason about software through formal specifications. Using an LLM does not get around the necessity of knowing what the LLM should generate, and ensuring that it does what you expect. Indeed, these are exactly the skills this course teaches.

The quizzes and exams are in-class and on paper, and compose the majority of your grade. Thus, any reliance on an LLM to the detriment of your learning will likely affect your ability to pass the course.

On the other hand, a strong grasp of the course material will prepare you well to use LLMs in the future. LLMs are not perfect, and often will generate code that is half-correct or missing an important corner case. The training you will receive in CS2800 will give you the tools and conceptual frameworks to effectively correct or rule out incorrect outputs from LLMs.

Classroom Environment

To create and preserve a classroom atmosphere that optimizes teaching and learning, all participants share a responsibility in creating a civil and non-disruptive forum for the discussion of ideas. Students are expected to conduct themselves at all times in a manner that does not disrupt teaching or learning. Your comments to others should be constructive and free from harassing statements. You are encouraged to disagree with other students and the instructor, but such disagreements need to respectful and be based upon facts and documentation (rather than prejudices and personalities). The instructor reserves the right to interrupt conversations that deviate from these expectations. Repeated unprofessional or disrespectful conduct may result in a lower grade or more severe consequences. Part of the learning process in this course is respectful engagement of ideas with others.

This policy applies to all course-related spaces, including office hours, any exam reviews, and certainly the course Discord.

Title IX

Title IX of the Education Amendments of 1972 protects individuals from sex or gender-based discrimination, including discrimination based on gender-identity, in educational programs and activities that receive federal financial assistance.

Northeastern’s Title IX Policy prohibits Prohibited Offenses, which are defined as sexual harassment, sexual assault, relationship or domestic violence, and stalking. The Title IX Policy applies to the entire community, including male, female, transgender students, faculty and staff.

If you or someone you know has been a survivor of a Prohibited Offense, confidential support and guidance can be found through University Health and Counseling Services staff https://www.northeastern.edu/uhcs/ and the Center for Spiritual Dialogue and Service clergy members https://www.northeastern.edu/spirituallife/. By law, those employees are not required to report allegations of sex or gender-based discrimination to the University.

Alleged violations can be reported non-confidentially to the Title IX Coordinator within The Office for Gender Equity and Compliance at: mailto:titleix@northeastern.edu and/or through NUPD (Emergency 617.373.3333; Non-Emergency 617.373.2121). Reporting Prohibited Offenses to NUPD does NOT commit the victim/affected party to future legal action.

Faculty members are considered "responsible employees" at Northeastern University, meaning they are required to report all allegations of sex or gender-based discrimination to the Title IX Coordinator.

In case of an emergency, please call 911.

Please visit https://www.northeastern.edu/titleix for a complete list of reporting options and resources both on- and off-campus.

Students with Disabilities

Students who have disabilities who wish to receive academic services and/or accommodations should visit Disability Access Services at 10 Dodge Hall or email DASBoston@northeastern.edu. If you have already done so, please provide your letter from the DAS to me early in the semester so that I can arrange those accommodations.