This course provides an introduction to the science of software. We will write programs and we will use logic to prove the correctness of our programs. We will also use logic to specify what correctness means.

We will learn by doing. This semester we will use the LEAN theorem prover. We will use LEAN's functional programming language to write simple programs, LEAN'S logic to write properties (specifications) of our programs, and LEAN's proof system to write proofs. Writing proofs is fun! It's like trying to find your way out of a maze. So we will basically be playing games all semester long, and in the process learning about functional programming, (simple) types, logic, proof tactics, recursion, induction, termination analysis, invariants, and other cool things.

The prerequisites are a basic familiarity with functional programming (CS 2500) and discrete structures (CS 1800). If you do not have this background, you need the permission of your instructor.

This semester we will use Canvas for most of the logistics. In particular, the syllabus is available on Canvas. Students taking the class are required to check Canvas daily for announcements, assignments, etc.

This semester lectures will follow the NUflex model: https://nuflex.northeastern.edu. Many things, like labs, office hours, etc, will be online. Details on Canvas.