3 ms·

First of all, you're assuming that the person who writes the theorems is always correct and is able to describe their code accurately. This is not the case. Sec

• voxcogitatio 16y ago
  Of course human error applies here too; But it's much simpler to get one type right than to use the type in the right way everywhere. Per example: The Red-Black-Tree implementation mentioned in the examples. If we define a tree that cannot be unbalanced, we can skip all explicit checks for whether the tree is balanced, thus eliminating a source for errors (forgetting/bungling the balance checks) and also increasing productivity (since we don't need to write the balance checks in the first place).
• loup-vaillant 16y ago
  > First of all, you're assuming No I'm not. When I say "no error", that include the specs. For instance, correctly following a specs when the green button set of the emergency shut down makes the interface too astonishing. That's a bug. > Second, it's way more easy to take a bunch of common sense measures than to deal with this. Of course. we never tried it seriously. What we didn't try yet is always more difficult. But if we do, it may very well become easier. I don't know. Anyway, these weren't the point. My point was that the domains where we need bug-free code is broader than we might think at a first glance. Not being able to trust that the code you run is error-free has costs that could very well be more important than taking the time to prove the absence of errors.