Finitism, imperative programs and primitive recursion

Following the Crisis of Foundations Hilbert proposed to consider a finitistic form of arithmetic as mathematics' safe core. This approach to finitism has often admitted primitive recursive function definitions as obviously finitistic, but some have advocated the inclusion of additional variants of recurrence, while others argued that, to the contrary, primitive recursion exceeds finitism. In a landmark essay, William Tait contested the finitistic nature of these extensions, due to their impredicativity, and advocated identifying finitism with primitive recursive arithmetic, a stance often referred to as Tait's Thesis. However, a problem with Tait's argument is that the recurrence schema has itself impredicative and non-finitistic facets, starting with an explicit reference to the functions being defined, which are after all infinite objects. It is therefore desirable to buttress Tait's Thesis on grounds that avoid altogether any trace of concrete infinities or impredicativity. We propose here to do just that, building on the generic framework of [13]. We provide further evidence for Tait's Thesis by outlining a proof of a purely finitistic version of Parsons' theorem, whose intuitive gist is that finitistic reasoning is equivalent to finitistic computing.