2 ms·

First, start with an automatic proof that the contract will halt... Oh wait

• WJW 5y ago
  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.
  • carnitine 5y ago
    Most real world programs, not most programs in general.
• TacticalCoder 5y ago
  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.
  • mst 5y ago
    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.
• mbrodersen 5y ago
  Easy. Just use a language that isn’t Turing complete or require a proof of termination. All solved problems in the proof community.