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. We will use the LEAN theorem prover. (We will use LEAN version 3.) 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.
We will use Canvas for most of the logistics. In particular, the syllabus will be available on Canvas. Students taking the class are required to check Canvas daily for announcements, assignments, etc.