Skip to content

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.

You may also like