> Most software is written in imperative Turing equivalent languages, so Turing Machines are involved all the time.

I don't understand what that means. Everything is "Turing equivalent" in some sense[0]. It's like saying that since every language can be compiled to C, then C is "involved all the time". That would even be more accurate, because our programs are most certainly not TM-equivalent. Proof: the asymptotic complexity of a real program and that of a Turing machine for most algorithms differs by a power of 2 or 3. Therefore, programs and TMs cannot possibly be equivalent. If you had said RAM machines at least you would have been somewhere in the ballpark, and RAM machines are not Turing machines (see https://en.wikipedia.org/wiki/Random-access_machine).

> The fact that most verification software is not capable of dealing with them, demonstrates a language issue.

But that is not a fact, because 99% of the thousands of very real, verified production systems being constantly worked on are written in imperative languages, and roughly 0-1% is written in functional languages. Quite the contrary, verification software handles imperative programs better than functional programs. You don't have to take my word for it. See what one Xavier Leroy (author of CompCert) says on the issue here[1] and here[2]. So far, verification in functional languages requires inordinate effort.

The question of how much verification is tied to language is very much an open question.

> I'm advocating modelling contracts with Logic, instead of Turing Machines as used by Ethereum.

I wonder what you'd say about temporal logic, which is not only the most popular logic in software verification but one that models state machines.

As to Turing machines, I don't think you understand what they are. A Turing machine is one particular automaton, a particular instance of an abstract state machine, and a universal computational model, which is usually applied directly only in computational complexity theory, where it serves as a common cost model. The lambda calculus is a rewriting system (typed versions of which can be tied to one particular kind of logical reasoning via the C-H correspondence), another universal model of computation, and -- guess what -- another instance of an (ND) abstract state machine!

In short there are many concepts here that you mix up. Turing machines, however, are one concept that is completely absent from both PLs and software verification (where it tends to turn up only in the marketing speech of some FP advocates). No one programs Turing machines. Program logics most certainly apply to imperative languages, and in fact, this is -- to date -- where they are most used, and quite successfully.

[0]: And if you're referring to total languages then you're confusing things further. Totality has little effect on verification; it is required in order to not introduce logical inconsistencies in typed lambda calculus, and is only relevant when dependently typed languages are used to prove general mathematical theorems -- not verify programs.

[1]: http://events.inf.ed.ac.uk/Milner2012/X_Leroy-html5-mp4.html

[2]: http://events.inf.ed.ac.uk/Milner2012/Monday_Panel-html5-mp4...