Presumably such a formalization is precluded by easy formalizations of executions of Turing machines; already computer scientists describe Turing machines and t

Presumably such a formalization is precluded by easy formalizations of executions of Turing machines; already computer scientists describe Turing machines and their executions in most proofs in extremely informal ways because of their tediousness. It would already be a miracle if we had clear formalizations of proofs of major complexity results regarding Turing machines.