Making Etherium contracts a full byte code execution engine was a big mistake. That form is too bug-prone and led to the DAO debacle. It should have been something simpler, such as a decision table. That simple declarative form can handle most useful business logic, but can't loop. It's always decidable and is easy to hand-check.
full byte code execution
engine was a big mistake
The proofs could be auto-generated for decision table based contracts, so a decision table could be a convenient DSL for simple contracts, without preventing more complicated contracts. The average contract writer would never need to see the full language or be exposed to proofs.