3 ms·

The Ethereum VM accepts opcodes like any other modern computing platform. There's a lot of work going into formal verification of contract code. There's nothing

The Ethereum VM accepts opcodes like any other modern computing platform. There's a lot of work going into formal verification of contract code. There's nothing in principle that prevents compilation of smart contracts into VM code via a formally verified compiler that implements a functional language.

KirinDave 9y ago
Except the majority of the Ethereum community being ideologically opposed...
- mbrock 9y ago
  What do you mean?
- DennisP 9y ago
  I'm an Ethereum smart contract dev/auditor and active in the community. I'm not aware of any ideological opposition to more functional or verifiable languages. In fact, there are several new languages in development to move things in that direction, including Vyper (originally designed by Vitalik) and Bamboo (designed by the person employed by the EF to work on formal verification).
  - KirinDave 9y ago
    My experience proposing actual use of these has been met with complaint and actual jeers in social circles. Further, it's pretty depressing that you suggest Vyper and Bamboo actually offer more formal verification or even correctness. I don't see either trying to adopt approaches more like Simplicity.