Kwangkeun Yi
Some 10 years ago, Harper illustrated the powerful method of proof-directed debugging for
developing programs with an article in this journal. Unfortunately, his example uses both
higher-order functions and continuation-passing style, which is too difficult for students
in an introductory programming course. In this pearl, we present a first-order version of
Harper's example and demonstrate that it is easy to transform the final version into an
efficient state machine. Our new version convinces students that the approach is useful,
even essential, in developing both correct and efficient programs.