If you can't prove the correctness of your program, you shouldn't run it. Why are you concerned with proving the correctness of arbitrary programs? Can you give

If you can't prove the correctness of your program, you shouldn't run it. Why are you concerned with proving the correctness of arbitrary programs? Can you give an example of an Ethereum-like program that can't be proven correct? Here's how reasonable Ethereum contract development should happen. You construct the contract, either in some high level language or in bytecode. Then you prove, using some reasonable formalism (TLA+, Isabelle, paper, symbolic execution, or whatever), that the contract does what it should do. Then people who want to trust the contract look at this proof. This is not at all hindered by the EVM being quasi Turing complete, because at no point do you have the question "How can I mechanically verify halting of an arbitrary program?"