Week 1: Why Our Code Breaks (and How to Fix It)

Overview

We motivate the entire audience (especially engineers and mathematicians) by showing the catastrophic failures of “correct-looking” code. Through compelling case studies, including the Ariane 5 rocket explosion, the Therac-25 radiation machine, and the Heartbleed bug, we’ll examine the limits of testing and introduce the concept of formal verification as a path to (almost*) truly reliable software.

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 21 January, 15:00 — 17:00 (Beirut time)
• Place: Engineering Lecture Hall (ELH)
• Online Meeting Link
• Recording

Core Concepts

• Real-world software disasters (case studies): Ariane 5 ($370M, integer overflow from reused code), Therac-25 (race condition, 6 deaths), Heartbleed (buffer over-read, 17% of servers exposed)
• Fundamental limitations of testing: finite inputs vs infinite possibilities, cannot test all executions/timing/concurrency, adversarial behavior, Dijkstra’s principle (testing shows presence of bugs, never absence)
• Formal verification foundations: mathematical proofs of program correctness, catching errors at compile-time, automated theorem proving (SAT/SMT solvers) vs interactive (proof assistants with guaranteed soundness)
• Introduction to proof assistants: Rocq/Coq, Isabelle/HOL, Agda, Lean4, Curry-Howard correspondence (programs = proofs)
• Why Lean4: combines automation with verification guarantees, small trusted kernel (De Bruijn criterion ~10k lines), practical programming language, modern and actively developed, Mathlib mathematical library
• Dependent types: types depending on values (Vector α n, Fin n, subtypes), encoding invariants directly in types, catching bugs at compile-time (“if it compiles, it’s correct”)
• What could have been prevented: turning catastrophic runtime crashes into compile-time type errors for all three disasters

Slides

Week 1 Slides: Download PDF

Readings

(To be provided in class)

Weekly Quiz

Quiz 1: Formal Verification Fundamentals

Quiz Link: Take Quiz 1

Deadline: Before Week 2 session
Passing Score: 60%

Programming Assignment

Assignment 1: Setting Up Your Lean Environment and Exploring Lean Zulip

Objective 1: Successfully install Lean4 and verify your setup is working correctly.

Tasks:

1. Install Lean4 following our guide
2. Install the VS Code extension for Lean4

Objective 2: Join the Lean community on Zulip and introduce yourself.

Tasks:

1. Create a free account on Lean Zulip
2. Navigate to the Lebanon thread in the Geographic locality channel
3. Post a “Hi” message with an optional short introduction (who you are, why you’re taking PROOF101, what interests you about formal verification)
4. Explore other channels and see what the global Lean community is working on

If you want to post a more general message, like:

Hello Lean community!

My name is X. I am Y at Z. My main interests are…

I am looking for … For example, …

Can anybody give me advice on the best way to go about something like this? …

Thanks, X.

Then, it is better to send this on the “New Members” channel of the Lean Zulip community. It is recommended to send both a messages (Lebanon thread in the Geographic locality channel and New Members channel), especially if you’re serious about learning and contributing to Lean.

Why this matters: The Lean community is incredibly welcoming and helpful. By introducing yourself, you’re not only connecting with fellow learners but also bringing visibility to formal verification work in Lebanon. Just like students at Saarland University do in the German channel, we’re building a presence in the Lebanese channel!

Resources:

• Official Lean4 Installation Guide
• Lean Zulip Community
• Lebanon Geographic Channel

Navigation

• Back to Course Overview
• Next Week: Week 2 →

Questions? Reach out on the course Discord!