If the language is Turing-complete there are definitely things you'll want in contract (such as the execution of it halting in finite time) that you won't be able to enforce. When code is the literal definition the contract, non-Turing complete is the way to go, because you can't reason about your code otherwise.

Turing-complete means you cannot write an algorithm to prove termination in every terminating case, but it doesn't mean you can't prove termination in particular cases, and it certainly doesn't mean you can't reason about your code.

Based on other comments here there certainly may be questionable decisions in the design of Solidity but that doesn't mean Turing-completeness is one of them.

Right. It will take time, but eventually Solidity (or some other alternative smart contracts approach) will likely be very trustworthy and secure.

I'm sorry but we have 6 decades of fundamental security research that has shown that it is essentially impossible to have a sufficiently complex, secure system.

The idea that we will ever stop needing human arbiters is laughable and pure hubris.

It's a matter of scope. You can build a secure currency exchange protocol: I have yet to hear of a technical issue with BTC that threatens its raison d'être. But when you're making a distributed, general purpose, scriptable contracting platform at some point you ought to consider trimming the core way down.

Maybe if the contracts had more constrained semantics ETH programming would be less scary, at the cost of some bells and whistles or more verbose syntax.

No, being Turing complete makes it impossible to be 100% secure and trustworthy, by definition.

It is possible to have trusted contracts, iff their logic is (mathematically) proven. But the VM can't make contracts more secure by itself.

> No, being Turing complete makes it impossible to be 100% secure and trustworthy, by definition.

Being Turing-complete means it's possible to write some contracts/programs for which certain features are undecidable by analysis.

It doesn't mean that programs that could be also be written in any more limited language can't have all the properties about then that could be proven in the non-Turing complete language proven when written in the Turing-complete language.

> It is possible to have trusted contracts, iff their logic is (mathematically) proven.

Trustworthiness of programs (including “smart contracts”, which are only loosely analogous to traditional contracts) is about whether the actual people using them get what they expect out of their behavior. Mathematical proofs of formal properties may be useful to that in some cases, but are not generally sufficient.

> It is possible to have trusted contracts, iff their logic is (mathematically) proven.

Suppose a non-Turing-complete language were used instead. Now, imagine a contract that is highly complex. If a layperson decides to trust that contract without reading the code, does it matter whether the language used to implement the contract was Turing-complete or not?

I'd argue that trust of contracts is pragmatically more of a social concept than a computational concept, since at scale the vast majority of contract users would make their trust decision about a contract based on non-technical factors.

> If a layperson decides to trust that contract without reading the code, does it matter whether the language used to implement the contract was Turing-complete or not?

Um, yes? Literally the point of weaker languages in this context is that they can be statically provable.

As would the same program written in a Turing-complete language. The Turing-completeness here is a total red herring.