Certain similarities between program verification and program synthesis are pointed out. The analogy is illustrated using a “bubble-sort” program. Recent work has shown that automatic deductive methods may be applied to the problems of program verification and program synthesis. As it turns out, these techniques are closely related. We demonstrate this relation using a particular program.