4 ms·
>a machine can check that code X matches definition Y You shouldn't just check against a definition Y. Ideally you'd have a set of properties that the contract
by logicchains 5y ago
>a machine can check that code X matches definition Y
You shouldn't just check against a definition Y. Ideally you'd have a set of properties that the contract must hold, then prove that X satisfies those properties. It's generally much easier to specify such properties than to write code implementing them, compare for instance an "is_sorted" function to an efficient "sort" function, so it's not just the same code written in a different language.
- dannyw 5y agoA "is_facebook" function may not be much easier. Smart contracts like Compound, Uniswap are complex functions; much more complicated than sorting which has an objectively correct answer.
- goldenkey 5y agoWe can do a probabilistic check. Just see how much data is being exfiltrated, if it's greater than a X% we can figure it's either Facebook or the Chinese government. ;-)
- cortesoft 5y ago> Ideally you'd have a set of properties that the contract must hold, then prove that X satisfies those properties. The issue is that how do you know you have the correct set of properties that a contract must hold? You might think you have all the properties that you need, but realize later that you missed one that is critical for your desired outcome.
- jkhdigital 5y agoFair enough, but that problem exists regardless of whether you’ve bothered to formally verify the functionality. Gathering requirements is hard, in other words.
- cortesoft 5y agoMy concern is that the verification will provide a false sense of security. This article, for example, seems to be arguing that the verification means there can’t be flaws. I think misunderstanding requirements is much more likely than they are making it seem.