4 ms·

A Bitcoin developer is working on a formally verifiable language: https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2017-October/015217.html https://lists

• digikata 9y ago
  Does this move the bugs from the implementation language to the language of the verification spec? Or is there a way to express some generic requirements such as "don't strand assets"?
  • mannykannot 9y ago
    Presumably one would have to first formalize that constraint (taking care, for example, that 'not stranded' is not being satisfied by someone stealing the assets), and then, unless the language makes it impossible, prove that it is not violated anywhere. In Solidity, it is a long deductive chain from the specific bug here to the realization that it could lead to stranding.
• scottlocklin 9y ago
  I'm not sure formal verification would have helped here. A linter would have helped.