I actually genuinely agree. Trustless computing is a very strong use case for systems where a lot more verification happens up front, because the downsides of messing up are so obvious and immediate.

It's worth noting that Ethereum's "fuel" model as a 1:1 correspondence with how Idris's mostly-total IO monad works. The "infinite fuel" bit can just be turned off and some (substantial and tricky, I admit) changes written to keep top-level state around and bam; timeboxed resume-able IO