Morgan’s refinement calculus (as described in his book, Programming from Specifications, available online) gives an elegant way to derive sequential programs from their specifications in a step-by-step way, ultimately resulting in a proven-correct implementation of the specification. This is still a manual process, though, where programs must be written and derived by hand, using pen-and-paper proofs. Proof assistants hold a lot of promise as tools to make proofs more rigorous and potentially more automatable. This project would consist of implementing Morgan’s refinement calculus in a proof assistant, to produce a program derivation framework where programs are stepwise derived from their specifications with tool support.
Expected knowledge would include: basics of using a proof assistant, such as Lean 4, Isabelle/HOL, or Agda. Experience with Hoare Logic would be nice, but is not required.