5 ms·
My understanding is that the halting problem does not prevent formal proofs of Ethereum contract correctness because Ethereum contracts have gas limits that mak
by Jabanga 9y ago
My understanding is that the halting problem does not prevent formal proofs of Ethereum contract correctness because Ethereum contracts have gas limits that make them terminating.
- dallashoxton 9y agoAnd the entire concept of 'gas' to me seems to be a hacky work-around in order to implement a Turing-Complete language on the blockchain. I'm not even sure it is needed -- the whole 'Turing-Complete' aspect of the EVM seems to be an engineering solution in search of a problem. And 'gas' is certainly not intuitive as a metaphor for end-users of Ethereum who would use it as a currency (how does a financial transaction "run out of gas", exactly?)
- Jabanga 9y agoGas is analogous to cycles of the EVM that the contracts uses when it executes. Someone suggested 'gas' should have been called 'cycles' to more clearly convey its meaning and avoid a lot of confusion. Anyway, gas/cycles must be limited given there are no access controls on use of the EVM. It's an effective DoS control. It's also orthogonal to Turing Completeness.