Week 9: Lean, Rust, and the Future of Reliable Software & Project Kick-off

Overview

We survey the broader ecosystem of formal methods and verification tools, understanding how Rust’s borrow checker acts as a lightweight proof system, and exploring other proof assistants in the landscape. Then we launch the final project where you’ll apply everything you’ve learned.

Lecturer

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

Session Information

Date and Time: Wednesday 23 March, 15:00 — 17:00 (Beirut time)
Place: IOEC (Oxy) 518
Online Meeting Link
Recording

Core Concepts

The verification landscape: brief overview of Coq/Rocq (mature ecosystem, CompCert), Agda (flexible syntax, HoTT), F* (systems verification, verified crypto), Dafny (automatic verification, SMT-based), Isabelle/HOL (strong automation), when each tool is used
The memory management problem: manual memory management in C/C++ (stack vs heap, pointers, use-after-free, double-free, memory leaks, 70% of security bugs), garbage collection in Java/Python/Go (automatic but runtime overhead, unpredictable pauses), tradeoffs between safety and performance
Rust’s ownership system: ownership rules (each value has one owner, owner deallocates when out of scope, moves on assignment), preventing use-after-free and double-free at compile time with zero runtime overhead
Rust’s borrowing system: shared references (&T) for read-only access, mutable references (&mut T) for exclusive write access, borrowing rules (either one mutable reference OR many immutable references, never both), preventing data races, and iterator invalidation at compile time
Lifetimes: tracking reference validity, preventing dangling references, lifetime annotations ('a) for explicit lifetime relationships, compiler ensures references never outlive data
Rust’s type system as practical compromise: memory safety without garbage collection, zero-cost abstractions, performance equivalent to C/C++, prevents 70% of security bugs (null pointers, use-after-free, data races) but cannot prove arbitrary properties like Lean/Rocq
The borrow checker as a lightweight proof system: affine types (ownership), linear logic (resources consumed once), connection to formal verification, automatic verification during compilation
Real-world adoption: Microsoft (Windows components), Google (Android), Linux kernel, AWS Firecracker, growing industry use due to memory safety guarantees
Final project kick-off: brainstorming session, project scope and requirements, choosing between math and algorithms tracks, optional Mathlib or CSlib contributions with Rida’s guidance, technical support

Slides

Week 9 Slides: Download PDF

Readings

Functional Programming in Lean 4 (Chapter 9)

Weekly Quiz

Quiz 9: Verification Landscape

Quiz Link: Take Quiz 9

Deadline: Before Week 10 session
Passing Score: 60%

Programming Assignment

Assignment 9: The Rust Programming Language & Final Mini-Project

Objective 1: Learn about practical applications of type systems through the Rust programming language.

Tasks:

Objective 2: Plan and scope your final verification project.