 In an attempt to mediate between conflicting foundational positions, Hilbert shifted issues, already around 1900, from a mathematical to a vaguely conceived metamathematical level. That approach was rigorously realized in the 1920s, when he took advantage of the possibility of formalizing mathematics in deductive systems and investigated the underlying formal frames from a strictly constructive, “finitist” standpoint. Hilbert’s approach raised fascinating metamathematical questions—from semantic completeness through mechanical decidability to syntactic incompleteness; however, the hoped-for mathematical resolution of the foundational issues was not achieved. The failure of his finitist consistency program raised and deepened equally fascinating methodological questions. A broadened array of problems with only partial solutions has created a vibrant subject that spans computational, mathematical, and philosophical issues—with a rich history.