Hilbert's Program was only that: a program or proposed course of action. Let us now ask: To what extent can the program be carried out? In order to study this question fruitfully, one must reformulate the program in more precise terms. I shall now do this.
Hilbert's description of the ``big system,'' corresponding to infinitistic mathematics, is already sufficiently precise. For my purposes here I shall identify the big system as Z2, i.e. second order arithmetic. Supplement IV of Hilbert and Bernays [15] shows that Z2 is more than adequate for the formal development of classical analysis, etc. It would not matter if we replaced Z2 by Z3, Z4, or even ZFC.
The unacceptable imprecision occurs in Hilbert's discussion of finitism. There is room for disagreement over exactly which methods Hilbert would have allowed as finitistic. This is not a defect in Hilbert's presentation. Hilbert's plan was to carry out a consistency proof which would be obviously finitistic. Had the plan been completely successful, there would have been no need for a precise specification of the outer limits of finitism.
At this point I invoke the work of Tait [25]. Tait argues convincingly that Hilbert's finitism is captured by the formal system PRA of primitive recursive arithmetic (also known as Skolem arithmetic). This conclusion is based on a careful study of what Hilbert said about finitism in [13,14] and elsewhere. There seems to be a certain naturalness about PRA which supports Tait's conclusion. PRA is certainly finitistic and ``logic-free'' yet sufficiently powerful to accommodate all elementary reasoning about natural numbers and manipulations of finite strings of symbols. PRA seems to embody just that part of mathematics which remains if we excise all infinitistic concepts and modes of reasoning. For my purposes here I am going to accept Tait's identification of finitism with PRA.
I have now specified the precise version of steps 2.1 and 2.2 of
Hilbert's Program. Step 2.3 is then to show that the consistency of
the formal system Z2 can be proved within the formal system PRA.
If this could be done, it would follow that every 
sentence
which is provable in Z2 would also be provable in PRA. We would
describe this state of affairs by saying that Z2 is
conservative over PRA with respect to
sentences. This
would constitute a precise and definitive realization of Hilbert's
Program.
Unfortunately, Gödel's Theorem [9] shows that any such
realization of step 2.3 is impossible. There are plenty of sentences which are provable in Z2 but not in PRA. (An example of
such a sentence is the one which asserts the consistency of the formal
system Z1 of first order arithmetic. Other examples, with a more
combinatorial flavor, have been given by Friedman.)
Note that Gödel's Theorem does not challenge the correctness of Hilbert's formalization of infinitistic mathematics, nor does it undercut Tait's identification of finitistic mathematics with PRA. Gödel's accomplishment is merely to show that the wholesale reduction of infinitistic mathematics to finitistic mathematics, which Hilbert envisioned, cannot be pushed through.
At this point I insert a digression concerning the relationship of Hilbert's Program to other reductionist programs.
In the philosophy of mathematics, a reductionist is anybody who wants to reduce all or part of mathematics to some restricted set of ``acceptable'' principles. Hilbert's plan to reduce all of mathematics to finitism is only one of many possible reductionist schemes. In the aftermath of Gödel's Theorem, several authors have proposed reductionist programs which are quite different from Hilbert's.
For instance, Feferman [5] has developed an elaborate program of predicative reductionism. (See also Simpson [22], pp. 152-154.) Certainly Feferman's predicative standpoint is very far away from finitism. It accepts full classical logic and allows the set of all natural numbers as a completed infinite totality. But it severely restricts the use of quantification over the domain of all subsets of the natural numbers. At this APA-ASL symposium, Feferman referred to predicative reductionism as a ``relativized'' form of Hilbert's Program.
Similarly Gödel [10] has proposed an ``extension'' of the finitistic standpoint, by way of primitive recursive functionals of higher type. Also Bernays [1], p. 502, has discussed a program of intuitionistic reductionism which he regards as a ``broadening'' or ``enlarging'' of proof theory. In his introductory remarks to this symposium, Sieg interpreted Bernays as calling for a ``generalized Hilbert program.''
I would like to stress that these relativizations, extensions and generalizations are very different from the original Program of Hilbert. Above all, Hilbert's purpose was to validate infinitistic mathematics by means of a reduction to finitistic reasoning. Finitism was of the essence because of its clear physical meaning and its indispensability for all scientific thought. By no stretch of the imagination can Feferman's predicativism, Gödel's higher type functionals, Myhill's intuitionistic set theory or Gentzen's transfinite ordinals be viewed as finitistic. These proof-theoretic developments are ingenious and have great scientific value, but they are not contributions to Hilbert's Program.