3 ms·

Could you give an example of a practical contract which demonstrates this problem? My contention is that the overlap between useful smart contracts and ones wh

• anyfoo 8y ago
  Could you give me an example of a practical program (none of that "hello world" or "multiply two numbers"-grade stuff) that has entirely been proven correct, through tests or formal methods? Let's start with tests: If you don't write a test for every single possible case, you will not know if there is not an edge case in your program that you did not catch. Unfortunately, the number of cases for any program that isn't entirely trivial (and thus mostly useless) grows so enormously quickly that you simply cannot write an exhaustive amounts of tests. So instead, you have to classify your inputs and test "representative" inputs for each of those classes. However, to make the reasoning of what is a perfect classification, i.e. a classification where each input you give in your tests behaves the same (for a reasonable definition) as any other input in that class, requires proving non-trivial properties about the program. And that, the halting theorem tells us, is impossible as well. In simpler words: In even relatively simple programs, there are more tests to write than available lifetime, but theory also tells us that we can't know how to reduce the test cases to only the interesting ones.