A tactic is any procedure which implements a correct search strategy. The goal of this paper is to provide a uniform framework where the user can hand-code tactics as programs in a metalevel programming language, can theorem prove them as terms in a first order classical metatheory, and is provided with a mechanism which allows for a bidirectional `translation` between the programming language and the logic. We call tactics of the first kind, `Program tactics`, those of the second kind `Logic tactics`. Inside this framework it is possible to use program tactics as terms inside Logic tactics and, viceversa, to use Logic tactics as programs inside Program tactics