The term_of operation enables two new modes of programming in in addition to the conventional mode of writing function terms. To program in the first new mode one writes proof outlines, p, which contain the computational information necessary for term_of(p) to be executable. The second mode is a refinement of the first in which complete proofs, cp, are supplied as arguments to term_of. In this case one knows that the program meets its specification, so this mode might be called ``verified programming''.