課程簡介Course Description

As software systems become increasingly critical to infrastructure, finance, and security, the ability to write code that is not just "functional" but provably correct is a defining skill for advanced computer scientists.

This course moves beyond standard software engineering practices to explore the mathematical and logical foundations of programming. We bridge the gap between implementation (writing code that runs) and specification (describing what code should do). The curriculum is divided into three interconnected pillars:

1. Functional Programming (TypeScript): We begin by disciplining state and side effects using strong static typing, algebraic data types, and monads.

2. Constraint Programming (Z3/SMT): We treat logic as a computational tool, using SAT/SMT solvers to model complex problems and synthesize solutions automatically.

3. Program Verification (Dafny): We culminate by combining programming and logic to write mathematically verified software, where the compiler guarantees correctness against a formal specification.

Course Objectives

By the end of this semester, students will be able to:

• Reason about correctness: Move beyond "testing cases" to proving properties for all possible inputs.

• Leverage type systems: Use advanced type theory (generics, ADTs) to make invalid states unrepresentable.

• Model problems logically: Translate real-world resource and scheduling constraints into First-Order Logic for automated solving.

• Verify algorithms: Use Hoare Logic and pre/post-conditions to mathematically prove the correctness of imperative algorithms.

Prerequisites

• Discrete Mathematics: Comfort with Boolean logic, set theory, and basic proof techniques (induction).

• Data Structures: Familiarity with trees, graphs, and standard algorithms (sorting/searching).

• Programming Maturity: Ability to write non-trivial programs.

• We will have lab sessions every week. Students will need a laptop to do these exercises.