Week 2: Functional Programming

Overview

We explore logic and programming paradigms as motivation (imperative, OOP, functional, etc.). Using Lean4, we cover the basics of functional programming and typed functional programming through The Hitchhiker’s Guide to Logical Verification chapter 5.

Lecturer

  • Daniel Dia — Course creator, primary instructor & organizer (American University of Beirut); Computer & Communications Engineering (CCE) and Mathematics dual-degree student (AUB).

Session Information

Core Concepts

  • Historical context (1936-2005): lambda calculus vs Turing machines (Church vs Turing, two models of computation), software crisis (1960s spaghetti code, GOTO statements), OOP dream vs reality (Smalltalk 1972 purity vs C++/Java corruption with mutable state), Tony Hoare’s “billion dollar mistake” (null pointers 1965), concurrency wall (2005, multicore requires immutability)
  • Pure functions and side effects: deterministic (same input → same output), no observable side effects (no mutations, I/O, external state changes), benefits (cacheable via memoization, portable with explicit dependencies, testable without mocks, reasonable via referential transparency, parallelizable safely)
  • First-class and higher-order functions: functions as values (stored in variables, passed as arguments, returned from functions), map (transform each element), filter (select by predicate), fold (reduce to single value, foldr vs foldl), compose (chain functions)
  • Currying and partial application: transform f:(α×β)→γ into f:α→β→γ (multiple arguments as nested functions), enables partial application (fix some arguments, get specialized function), utility functions (curry, uncurry, flip, const)
  • Inductive types in practice: enumerations (Weekday, Color), structures (Point with fields, functional update syntax), sum types (Sum α β with inl/inr constructors), Option types (none/some, fixes null pointer problem), recursive types (Nat, List, BTree), polymorphism with type variables
  • List and tree operations: map, filter, fold, zipWith, dropWhile, partition, interleave, splitAt, findIndex, tree operations (size, height, mirror, mapTree), tree traversals (inorder for BST, level-order breadth-first)
  • Pattern matching and mathematical induction: pattern matching on constructors (exhaustiveness checking), structural induction on lists (base case [], inductive case x::xs), structural induction on trees (base case empty, inductive case node with subtrees)

Slides

Week 3 Slides: Download PDF

Readings

  1. Functional Programming in Lean 4 (Chapters 1-2-3 + Interlude 1)
  2. Theorem Proving in Lean 4 (Chapter 4)
  3. The Hitchhiker’s Guide to Logical Verification (Chapter 5)

Weekly Quiz

Quiz 3: Functional Programming & λ-Calculus

Quiz Link: Take Quiz 3

Deadline: Before Week 3 session
Passing Score: 60%

Programming Assignment

Assignment 3: Functional Programming in Lean

Objective:

Assignment: PROOF101 Programming Assignment 3

Questions? Reach out on the course Zulip!