> You already know why they halt: there's a gas limit. Did you actually read my post? I'm not claiming halting is a problem; it's merely an example of undecida

> You already know why they halt: there's a gas limit. Did you actually read my post? I'm not claiming halting is a problem; it's merely an example of undecidability. The "gas limit" doesn't help in the cases where the program does halt with unexpected behavior. > Turing complete programs don't generally halt. That's the definition. Where did you get this nonsense? See [1] for the actual definition. > attack was an extremely simple programming error Yes, which is why it's stupid to use a language with a grammar that cannot be proven. If trivial mistakes happened in production code, how do you expect to find the subtle bugs that happen because of the complex interactions that occur in recursively enumerable grammars? > prove the correctness of programs You can do that for some programs, but not all. The point about grammars is there are classes of grammar that allow automatic verification. Using a recursively enumerable grammar instead of a regular or context-free grammar demonstrates a severe misunderstanding of either language theory, or secure/safe engineering practices. int_19h description[2] of some of the insane parts of Solidity suggests a PHP-style fractal of bad design[3], not a platform for proving correctness. [1] https://en.wikipedia.org/wiki/Turing_completeness#Formal_definitions https://en.wikipedia.org/wiki/Turing_completeness#Formal_def... [2] https://news.ycombinator.com/item?id=14810008 https://news.ycombinator.com/item?id=14810008 [3] https://eev.ee/blog/2012/04/09/php-a-fractal-of-bad-design/ https://eev.ee/blog/2012/04/09/php-a-fractal-of-bad-design/