 Weir argues (2010; 2016) that finitist formalism is not only extremely radical, it is incoherent. The reason is the all-pervasive role of abbreviation which generates complex tokens where most of their subparts will never exist, for example abbreviations which create numerals naming (speaking with the platonist) arbitrarily high numbers. As a result, strict finitist specifications cannot be given in the usual inductive fashion, as the intersection of all inductive sets containing the base set and closed under the complexity-forming operations. And this in turn means we cannot prove even very simple facts about wffs and proof.