Syllabus🔗

1 Course Description🔗

This course is about formal specification, and how logic can be used to help reason about software. Logic is presented from a computational perspective using property based testing, a technique available via libraries in nearly every programming language.

We focus on this form of computational formal methods in order to show how logic can be used to actively reason about software, rather than existing as a purely theoretical pursuit off to the side. Clearly, logical reasoning has value even outside of the context of the tools that we will use, but we think that these tools will allow us to gain a much more hands-on understanding of it than via a more traditional presentation, e.g., paper and pencil logic presentations you might find in a formal logic class in Philosophy.

The goal of the course is to introduce fundamental, foundational methods for both modelling and reasoning formally about computation. We want to be able to talk precisely about what programs should do, and once we learn how to express ourselves in precise specifications, we will deploy an array of techniques to use those specifications to increase the reliability of the programs we write.

We will draw upon propositional, first order, and higher order logics. We will talk about the strengths and limitations of various techniques, and how they can be applied to different problems.

2 Course Objectives🔗

The goal of the course is to introduce students to the logic and specification using the field of formal methods. While there are many human processes for increasing the reliability of software, formal methods begins from the premise that we can use math and computation to make software more reliable scientifically.

Students will learn how to formulate specifications as executable predicates in property based testing frameworks that they can bring to any programming language they use.

Every step of the way, we will be running our assertions and getting feedback as to whether they hold, so students will get hands-on experience with these state-of-the-art tools. At the same time, they will learn how these techniques can be used via libraries that they can easily bring to coop, jobs, and beyond.

3 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. If you did not do CS2500 using the Racket Teaching Languages (BSL, ISL, ISL+) there will be a brief (async) review at the beginning, as the programming in the course is based on an extension of ISL+.

4 Course Websites / Tools🔗

4.1 Website🔗

This website will be the main place that all course materials will be: homework assignments, lecture notes, etc. Please check it regularly.

4.2 Discord🔗

We will use Discord for announcements, questions, and discussion. While we will do our best to answer questions asked there, TA office hours are usually a much more reliable way to get help. You can use this link to join:

https://discord.gg/jz3qRar2c7

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

4.3 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 class. The Gradescope enrollment is based on Canvas, so if you just enrolled in the class, it might take a day or two to synchronize.

5 Software Used: Logical Student Language (LSL)🔗

6 Evaluation🔗

Your final grade will be (TENTATIVELY) calculated as follows:

Quizzes will occur every other week, on paper, at the beginning of class, and will be very short. We will drop the lowest quiz grade.

Exams will be in-person, during class. Doing better the second exam can raise your final score on earlier exams: essentially, your final exam 1 score will be the maximum of the average of that exam and exam 2 and the original score. Concretely, the formula (with examples) is:

(: exam1-final (-> Real Real Real))

;; the max of: original exam1 score, average of exam1 & exam2

(check-expect (exam1-final 95 90) 95)

(check-expect (exam1-final 80 100) 90)

(check-expect (exam1-final 80 90) 85)

(define (exam1-final exam1-raw exam2-raw)

(max exam1-raw

(/ (+ exam1-raw exam2-raw) 2)))

(: exam2-final (-> Real Real Real))

;; just the original exam2 score

(check-expect (exam2-final 100 80) 80)

(check-expect (exam2-final 80 100) 100)

(check-expect (exam2-final 70 80) 80)

(define (exam2-final exam1-raw exam2-raw)

exam2-raw)

Final grades will then be assigned on the following scale:

6.1 Homework🔗

Homework is a way to practice the material that you learn in lecture, and the main way you will learn the material. In is primarily a learning tool, and secondarily an assessment (i.e., grading) tool.

Homeworks can be done either solo or in groups of two – it’s up to you how, or if, to form groups: but if you do, please submit as a group on Gradescope (one person submits, add the other to the submission).

6.2 Exams🔗

There will be two exams, held on 2/20 and 4/7 (see Schedule for that and much more). They will be proctored and in-person.

7 Policies🔗

7.1 Late Work🔗

Any assignment can be turned in up to 24hrs late. After that 24hrs, no work will be accepted (except in truly exceptional situations), so be sure to start early and try to get all the work done by the deadline. If you decide to treat the late deadline as the normal deadline (asking for leeway on turning it in beyond the late deadline), expect not to be accomodated.

7.2 Regrades🔗

Sometimes mistakes can happen. Please don’t be afraid to reach out to a member of the instruction team for further explanation. If you believe an error was made, you may make a regrade request: be precise about what exactly you believe was the mistake. Do not abuse this. You must submit any requests for regrading at most 7 days after the feedback was released.

You submit regrade requests directly via Gradescope – that will automatically go to the person who graded your work. If the individual is unable to address your concerns you can approach your instructor for further assistance.

7.3 Collaboration🔗

You may discuss homeworks, including solutions, but may not either share or look at any code, aside from, of course, with your partner if you are working in a pair. You should keep your discussions to the approaches you took, ideas that are relevant, etc. You should not be discussing things in such detail that your solutions look identical.

Homework is the primary way you learn the material, and if you share solutions, not only are you violating academic integrity, you are preventing the person you are sharing them with from learning the material. Note: you may not work around this policy by dictating solutions: this is effectively the same as sharing code.

This is a relatively flexible policy, which we follow because working with others can often be one of the best ways to learn, and we’d love if you can benefit from peers as much as you can from the instruction team. Homework is one of the primary tools for learning this material, and we don’t want to take learning opportunities away from you.

That also cuts in a different direction. If you never figure out any solutions yourself and your conversations with others are always one-sided, you will likely suffer in the quizzes and exams, which account for 70% of your grade. So be sure you are using this policy to improve your learning via homework, rather than using it to avoid the learning opportunity of homework, as trying to "game" this collaboration policy is not a good way to be successful in the class.

7.4 LLMs🔗

You may not use LLMs (ChatGPT, or similar) for any portion of the course: assistance on homework, clarification of material, etc, unless explicitly told to in an assignment.

The entire point of this course is to teach you how to reason about and specify software: exactly the skill that will remain wholely relevant in an era increasingly dominated by these tools. Using an LLM does not get around the necessity of knowing what the LLM should generate, and ensuring it does what you expect: exactly the skills this course teaches.

But the nature of courses (and this one is no different) is that we have to give small, well-defined problems: our descriptions, while great practice for developing skills that will scale to much more complex problems, are also good prompts to LLMs.

If you use these tools, not only will you not learn anything (and thus, be no better off in real jobs, where these skills will be critical, especially for using LLMs effectively), but our quizzes and exams, which are on-paper, collectively compose 70% of your grade. So if you don’t learn the material (which you will fail to do if you heavily rely on LLMs), you will fail the quizzes and exams, and likely fail the course.

8 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.

8.1 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.

8.2 Students With Disabilities🔗

Students who have disabilities who wish to receive academic services and/or accommodations should visit the Disability Access Services at 20 Dodge Hall or call (617) 373-2675. If you have already done so, please provide your letter from the DRC to me early in the semester so that I can arrange those accommodations.