Automatic Synthesis of Recursive Programs: the Proof-Planning Paradigm