We’re continuing our series on verifying Richard Bird’s Pearls of Functional Algorithm Design — exploring elegant algorithms through the lens of formal verification in Dafny. This session focuses on two intriguing problems:

• Pearl 11 – Not the Maximum Segment Sum
• Pearl 2 – A Surpassing Problem

Both pearls highlight the power of functional thinking and the challenge of turning concise, declarative definitions into provably correct imperative or recursive implementations. What we’ll do:

• Review the original algorithmic ideas from each pearl.
• Implement and verify them in Dafny, specifying correctness conditions and reasoning about sequences and recursion.
• Discuss proof decomposition, invariants, and how to express high-level functional properties as formal specifications.
• Work individually or in small groups — sharing progress, insights, and obstacles along the way.

Why attend: If you enjoyed our first Pearls session or want to see how Dafny bridges elegant theory with verifiable code, this is a great next step. You’ll gain hands-on experience transforming functional specifications into verified implementations and deepen your intuition for proof-driven development.