In this paper we propose an interactive approach to program synthesis: Explicit strategies are used to guide program construction. Our approach regards program synthesis as a constructive theorem proving task. By specifying proof strategies in a higher order functional meta-language, we are able to represent the programmer s advice, mathematical inductions, program transformation rules/strategies and resolution methods in a uniform manner. The implementation of strategies depends on higher order unification.Our approach can be automatized easily.