11 ms·
If the proof is more complex than the software, I don't see how that gains you anything. It's harder to verify that you've proved the right thing than to verif
by zestyping 8y ago
If the proof is more complex than the software, I don't see how that gains you anything. It's harder to verify that you've proved the right thing than to verify the software itself, so how does that help?
- crimsonalucard 8y agoIn a type checked language. Your software is guaranteed to have no type errors. How hard was that?
- zestyping 8y agoThat's a great example! It illustrates the point in a better way than I tried to. A necessary part of why types are so useful is that understanding the types is easier than understanding the code itself. If the types become so complex that they start to get harder to understand than reading your code (e.g. C++ template errors can sometimes get this bad), then they are no longer helpful.