Earlier quoted context omitted.
There are languages which are both expressive and Turing incomplete, for example Coq. In the Coq language, Turing incompleteness is actually needed to be able to make complete proofs. Maybe Solidity would have been better implemented within Coq, but it's too late now.
Is it too late now? It seems to me that it should be possible to implement a better language on top of the existing system, there are plenty of languages that compile to JavaScript after all, so it's still worth discussing what a better language might look like. You say Coq is expressive; okay, but in what sense, for what purposes? A language which isn't Turing complete - or even one which is - isn't going to be expr…
In particular, Solidity is statically typed.
I would say that smart contracts are a lot like event processors that update bits of contract-local state and enforce preconditions. They are run in a single "thread" in blockchain order, but they can also invoke each other reentrantly (and that's the major source of confusion so far, so it should be limited and made very explicit).
Some contracts perform more complex calculations, e.g. I know of one that calculates compound interest using fixed point math.
There might be room for several different simpler languages for different purposes... It would make sense to use the most restricted language that can express the contract you want.