Great explanation! I would also add that the code does not necessarily have to be turing complete. There is a new language that complies to EVM bytecode that is decidable (not turing complete) https://github.com/ethereum/viper

It's a little less expressive, which makes it safer. Easier to reason about the code, for example)