Turing machines are arbitrary in that they don't derive from some mathematical basis. You could easily reformulate the abstraction in many different ways, replacing "tape" or a "read/write head" with some other quasi-physical concept that don't normally appear in mathematics. Those concepts are spurious, just provided for their analogy to real-world machines.
You can provide formal descriptions for many things - the Perl programming language, for example. I would also call that language unmathematical. You can study such objects mathematically, but they are essentially external objects of study which one is using mathematics to make more tractable.
In contrast, Curry and Howard discovered direct correspondences between logic and lambda calculus. For example, intuitionistic natural deduction is isomorphic to typed lambda calculus. The internal languages of Cartesian closed categories are lambda calculi.
If Church hadn't discovered lambda calculi, they would have eventually been discovered via one of these correspondences.
* Girard-Reynolds System F as a common language for both second-order propositional logic and polymorphic lambda calculus
* higher-order logic and Girard's System Fω
* inductive types as algebraic data type
* necessity in modal logic and staged computation
* possibility in modal logic and monadic types for effects
* The λI calculus corresponds to relevant logic.
* The local truth (∇) modality in Grothendieck topology or the equivalent "lax" modality (◯) of Benton, Bierman, and de Paiva (1998) correspond to CL-logic describing "computation types".
As such, lambda calculi are inextricably embedded in mathematics and logic, and their core features (ignoring superficial choices such as syntax) are a discovery, rather than an invention. We can't change the equivalences described above, they are facts that arise from the formalisms developed to address subjects like logic and categorical analysis. The same is not true of Turing machines.
You can provide formal descriptions for many things - the Perl programming language, for example. I would also call that language unmathematical. You can study such objects mathematically, but they are essentially external objects of study which one is using mathematics to make more tractable.
In contrast, Curry and Howard discovered direct correspondences between logic and lambda calculus. For example, intuitionistic natural deduction is isomorphic to typed lambda calculus. The internal languages of Cartesian closed categories are lambda calculi.
If Church hadn't discovered lambda calculi, they would have eventually been discovered via one of these correspondences.
Wikipedia provides a partial list of these correspondences at https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... :
* Girard-Reynolds System F as a common language for both second-order propositional logic and polymorphic lambda calculus
* higher-order logic and Girard's System Fω
* inductive types as algebraic data type
* necessity in modal logic and staged computation
* possibility in modal logic and monadic types for effects
* The λI calculus corresponds to relevant logic.
* The local truth (∇) modality in Grothendieck topology or the equivalent "lax" modality (◯) of Benton, Bierman, and de Paiva (1998) correspond to CL-logic describing "computation types".
As such, lambda calculi are inextricably embedded in mathematics and logic, and their core features (ignoring superficial choices such as syntax) are a discovery, rather than an invention. We can't change the equivalences described above, they are facts that arise from the formalisms developed to address subjects like logic and categorical analysis. The same is not true of Turing machines.