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: Monday 30 March, 15:00 — 17:00 (Beirut time)
• Place: Online
• Online Meeting Link (Meeting number: 2399 170 2835; Password: 4mYJSUyx35@)
• Session Recording (Password: RkKkC6W@)

Core Concepts

• The verification landscape: brief overview of Coq/Rocq (mature ecosystem, CompCert, Iris), Agda (flexible syntax, HoTT), F* (systems verification, verified crypto), Dafny (automatic verification, SMT-based), Isabelle/HOL (strong automation), and where Lean4 fits among them
• Rust’s ownership and borrowing systems: solving the problem of mutable aliased state via affine types (ownership) and region-safe aliasing (borrowing), enforcing the central invariant of any number of shared references (&T) XOR exactly one mutable reference (&mut T), preventing “spooky action at a distance” and iterator invalidation at compile time
• Lifetimes and the Curry-Howard isomorphism: lifetimes as region variables solving a constraint system over a partial order, traits as proof obligations (typeclass instances) checked at compile time, and the borrow checker acting as an automated decision procedure for a fragment of intuitionistic linear logic
• Rust and the verification ecosystem: RustBelt proving semantic soundness in Rocq using Iris, and the framing problem being solved for free by the borrow checker, enabling tools like Aeneas to translate mutable borrows into pure functions for formal verification in Lean4 without manual separation logic
• Final project kick-off: project scope and requirements, choosing between math and algorithms tracks, optional Mathlib or CSlib contributions with Rida’s guidance (for later).

Slides

Week 9 Slides: Download PDF

Readings

1. Functional Programming in Lean 4 (Chapter 9)
2. "Ownership" (by without.boats)
3. "References are like jumps" (by without.boats)

Programming Assignment

Assignment 6: Pitch and Create Your Final Mini-Project (Deadline: Sunday, 5 April)

Objective: Plan and scope your final verification project.

Tasks: Write your final project proposals. See the “Final Projects” page for more details.

Navigation

• ← Previous Week: Metaprogramming in Lean and Decision Procedures
• Back to Course Overview
• Next Week: Project Showcase & Wrap-up →

Questions? Reach out on the course Discord!