if you set out to prove "predicates" about a program, there are two (common) ways to go about it.

the first way involves writing a program, and then either in the language of the program or some other "more logical" language writing down some formula about the program and trying to construct a proof. proofs performed in this order are constructed by repeatedly reducing the terms of the proof towards axioms. you are given a list of transformations on the formula which are permitted, with the understanding that rewriting a formula in some sense preserves "truth", or at least logical implication. once you arrive at a formulation which is all axioms or instances of abstract axioms, you are done your proof. sometimes you have tool support to automate reducing the tedious parts of your formulas to axioms. formal systems which are intended to work this way include ACL2, Coq, HOL, NuPRL, Isabelle, Twelf, and many other logic and meta-logic frameworks.

the second way involves writing a formula expressing the conjunction of facts you eventually want your program to satisfy, and transforming that formula into the program by successive refinements (rewrites). you are given, like in the first case, a list of the sorts of syntactic transformations which constitute a legal refinement, with the understanding that a refinement of a term "means the same thing", only the refinement is "more concrete" than the refined. when you have nothing left but terms in your abstract machine language, you have completed the refinement and you can probably run the resulting program. some times you have tool support to automate performing tedious refinements of formulas into machine code. formal systems which are intended to work this way include Z, VDM, RAISE, B Method, Refinement Calculus, and Hehner's "practical theory of programming".

typically the underlying logics of members of either such family permit their use in one approach or the other, but the tools and logics may display the preference of their creators.