3 ms·
Do you have any views on Solidity as a contract language and how suitable it is for being formally verified? Does it make any properties you want to check diffi
by seanwilson 9y ago
Do you have any views on Solidity as a contract language and how suitable it is for being formally verified? Does it make any properties you want to check difficult or impossible to verify?
My experience with formal verification is that the further a language is away from being a pure functional language with easy to check termination, the more difficult you make life for yourself. You really want a smart contract language that was specifically created to be easy to formally verify rather than trying to tack on formal verification later.
- ptsankov1 9y agoNote that tools like Securify work directly on the EVM, and are therefore agnostic to the high-level language the contract is written in. The EVM itself is not as amenable to formal analysis (no types, explicit function calls, etc.).