[ddeyar]

> Imperative languages can also be formally verified. See the K framework for formal modeling and verification of EVM smart contracts.

Good to see that eth has the possibility too. It's a must have in my opinion.

> Beware, the gas price might be low because there is no volume. Binance Smart Chain had a lot of difficulty the past 2 days because they underpriced gas cost and basically DOS-ed themselves:

I don't know how tezos would react when DOS-ed. The next upgrade brings some further optimizations with it. Gas will then be calculated using saturated arithmetic.