Outlines the consequences of taking formalism in mathematics seriously. Gap between formalism and mathematical practice; Use of digital computers in proving theorems; Hierarchically arranged data banks of theorems and interactive programs; Finitary dogma's assertion that every recursive function is effectively computable; Church's thesis; Finitary consistency proof for Robinson's theory Q.