Verification Hack and Learn: Implementing Pearls of Functional Algorithm Design

We’re starting a new Hack and Learn series focused on implementing and verifying algorithms from Richard Bird’s Pearls of Functional Algorithm Design — a classic collection of elegant, deceptively simple problems in functional programming.
In this first session, we’ll tackle:

• Pearl 9 – Finding Celebrities
• Pearl 11 – Not the maximum segment sum

The goal:
Implement and verify these pearls in Dafny, exploring how the language’s specification and proof system can capture the properties that make these algorithms correct.
How it works:

• Each participant (or small group) chooses one of the pearls to work on.
• Try implementing the algorithm and formally specifying its correctness.
• We’ll share approaches, common pitfalls, and verification strategies as we go.
• By the end, we’ll compare notes and discuss what worked, what didn’t, and how Dafny’s features (like inductive proofs, sequences, and ghost code) help us reason about these classic problems.

Who it’s for:
Anyone interested in functional programming, algorithms, or formal verification. You don’t need to be a Dafny expert — just bring curiosity and a willingness to experiment.
Why attend:

• Learn how to translate elegant functional ideas into verified code
• Practice using Dafny for structured proofs
• Collaborate with others tackling similar challenges
• Help build a library of verified algorithmic “pearls”

Bring your laptop, your copy of Pearls of Functional Algorithm Design (if you have one), and your favorite reasoning tricks. Let’s hack, prove, and learn — one pearl at a time.