I have read many places that the decision for Ethereum to use a Turing-complete programming language sparked a lot of concerns over security. From my understanding, not using a Turing-complete programming language leads to a more secure network. Why is this the case?
It is much easier to formally verify the behavior space of Bitcoin script vs. Solidity.
For example, the DAO project suffered from reentrancy vulnerabilities, given that one could not predict the behavior of anonymous smart contracts when they were called/sent funds to (fallback function, now deprecated).
There are formal verification efforts for Solidity, but this increases the design difficulty tremendously, and one must ask whether it is worth the turing-completeness.