The system acts as a program synthesizer in the following sense. Given a computationally meaningful assertion (e.g., a ``program specification'' ) and an applicable proof tactic which produces at least the executable parts of a proof of the assertion, the extractor will produce from the proof a program. If the proof is complete then the program meets the specification. In this sense we have written a variety of program--synthesizing tactics. Several interesting comparisons can be drawn between these techniques and those based on classical methods, as in [Manna & Waldinger 80,Manna & Waldinger 85].