Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm