You jest, but the halting problem is only unsolvable in the general case. For "most" (but not all) programs it is perfectly possible to prove whether or not they will halt.

Most real world programs, not most programs in general.

The halting problem in Ethereum is "solved" (more like "dealth with") by a very simple technique: every EVM instruction has a cost and you have to provide "gas" to run your smart contract. If you don't provide enough gas, your contract call has zero effect and all the gas you paid is lost.

A contract call that would misbehave is guaranteed to halt: not by itself, but by the EVM, which, when the contract call eventually runs out of gas, shall take care of halting it.

It's pretty nice I'd say.

IIRC erlang does reduction based scheduling except with a multiplier related to the number of messages in its mailbox - would be interesting to read a comparison from somebody who understands the runtimes better than I do.

Easy. Just use a language that isn’t Turing complete or require a proof of termination. All solved problems in the proof community.