 One strategy for dealing with these problems is to combine formalism with strict finitism (for one brand of which see Yessinin-Volpin (1961; 1970) and for criticism Dummett (1975): only feasibly long “digestible” tokens—of formulae and of proofs—exist. Formulae with no feasible proofs or disproofs simply lack truth value. Since we know from Gödelian speed-up considerations that for many a provable sentence the shortest derivations of it or its negation are vastly longer than the sentence itself, this finitist/formalism position threatens to cause havoc across large areas of perfectly ordinary mathematics. 