Verification Hack and Learn: Pearls of Functional Algorithm Design in Dafny (2)
Details
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.