The close relationship between writing programs and proving theorems has
frequently been cited as an advantage of functional programming languages. We
illustrate the interplay between programming and proving in the development of
a program for regular expression matching. The presentation is inspired by
Lakatos's method of proofs and refutations in which the attempt to prove a
plausible conjecture leads to a revision not only of the proof, but of the
theorem itself. We give a plausible implementation of a regular expression
matcher that contains a flaw that is uncovered in an attempt to prove its
correctness. The failure of the proof suggests a revision of the
specification, rather than a change to the code. We then show that a program
meeting the revised specification is nevertheless sufficient to solve the
original problem.