[emilypi]

We're seeing a small cottage industry of state-machine verification techniques presenting themselves over the past year. K-framework has its accessibility proofs (ranging over the state space of possible program paths), Manticore has its symbolic state analysis, and a few others do roughly the same thing. None of these frameworks are focusing on improvement of the language or supplementing its features - they're just trying to make up for how easy it is to write bug-ridden EVM contracts! Good on them, but it points to how fundamentally flawed the EVM is by design.

[dguido]

FWIW I agree with the intent of this statement. The odd lesson we've learned is that extreme testability can overcome broken tools to create secure code. It's not the outcome you would expect since the orthodox in security engineering is that it depends on secure programming languages, frameworks, and compilers, which we have none of in Ethereum. But somehow people are carrying around hundreds of millions of dollars in smart contracts secured with high-powered testing and verification techniques. It's very weird.

I explored this topic a bit in a keynote earlier this year: https://github.com/trailofbits/publications/blob/master/pres...

I will also note that our long-term goal for Slither is to directly address some of the problems in Solidity (https://github.com/crytic/slither). It's like 2/3rds of a compiler already. It just needs a little extra push and we can generate EVM bytecode, then start ripping features out of the language that just aren't safe to use. It's amazing how far Ethereum has come with insecure tools but extreme testability. It begs the question what it would look like with both? I know Kadena is going for the clean slate approach (and we're keeping an eye on you all) but our investment at the moment is in adjustments to the current ecosystem.

[nickpsecurity]

The problem is likely that the platform won, it has a big ecosystem of tooling developing around it, and targeting it is best route. Maybe they can make a better language that compiles to it. Meanwhile, tool vendors are making tools that correct for flaws in the language rather than a little-known one. Also, given the tools out there, using the platform language with the tools might be safer than the other language.

The language I encouraged people to use for smart contracts was SPARK Ada. It's a mature language used in many industrial projects. Verification is easier with it. Building on what it already had would've cost them less and reduced risk. A SPARK Ada to EVM compiler is all they needed.

[DennisP]

The EVM is just a virtual machine. People are working on languages with less opportunity for bugs than Solidity, like Flint: https://github.com/flintlang/flint

Also Vyper, which doesn't go as far but is already used in production: https://github.com/ethereum/vyper

The EVM itself isn't the end of the road either. Over the next couple years, Ethereum is migrating to a more scalable sharded version using proof of stake, and it looks like that will allow pluggable execution engines.

[mirekrusin]

It's like saying that "assembly is fundamentally flawed" because people came up with haskell.

[emilypi]

It's in the sense that it's extremely difficult to write a program and fully understand what it's doing - that's why higher order representations and correct-by-construction languages were invented. Rather than putting bandaids on it with secondary and tertiary frameworks, languages like Haskell were built to be correct by construction.

But then there's the question of whether any of those flaws are even reasonable to take upon your contract when you consider their use-case within a blockchain context. If you're only ever running terminating programs, why expose the entire language to the attack surface of non-determinism and re-entrancy bugs when there are very reasonable and expressive CbyC languages available?

[mirekrusin]

EVM is not a language. EVM is deterministic otherwise the whole Ethereum would not function at all. Your criticism is directed more towards ie. Solidity. However alternatives are not availble as far as I know. There are some research projects but everything in this area is in alpha-research state.

[emilypi]

The problem is with the structure of the VM and its bytecode language. There are additional problems with Solidity, but the VM itself is the problem. Solidity only amplifies a poor architecture: https://medium.com/kadena-io/the-evm-is-fundamentally-unsafe...

[DennisP]

Vyper is available now. https://github.com/ethereum/vyper