3 ms·

> To me, essential to delivering a good product is detecting and killing defective code before delivery. The problem is that you cannot prove the non-existence

by Aaargh20318 9y ago

> To me, essential to delivering a good product is detecting and killing defective code before delivery. The problem is that you cannot prove the non-existence of bugs, even if you formally verify all your code, you've only proven that it conforms to spec, not that the spec is flawless. This is why you should always code defensively. Assume all code is buggy and take steps to deal with that. Code is written by humans, and humans make mistakes. That doesn't mean that you shouldn't try to deliver a flawless product, only that you should acknowledge the fact that you're going to fail.

eru 9y ago
Your argument would be in favour of a defensive spec, not in favour of a defensive implementation. To explain: your spec will have a few hygiene clauses like 'no stack overflow' or 'no crashes' and some things about what useful things the program should actually do. The latter is hard to formalise and deserve defense in depth. Lots of the former are easy to formalise and you can rely on the compiler to get it right. And that's what we are doing already anyway: even in C we just trust that a loop will compile to the appropriate conditional jumps and don't add defensive measures to check that.
- Aaargh20318 9y ago
  The point is that you're not going to do formal verification of your software. There is actually very little formally verified software out there, and the verified code that does exist is relatively small. And no, you can't rely on the compiler to get it right. Maybe if you only write Haskell you can get there 99% but there will always be human errors in code that the compiler can't find.
  - eru 9y ago
    We rely on computers to get parts of our spec right all the time. Yes, a higher level language lets you offload more to the computer (like Haskell), but even in C we are doing some off that. Yes, in practice you seldom have much of a formal spec, agreed.

eru 9y ago

Your argument would be in favour of a defensive spec, not in favour of a defensive implementation. To explain: your spec will have a few hygiene clauses like 'no stack overflow' or 'no crashes' and some things about what useful things the program should actually do. The latter is hard to formalise and deserve defense in depth. Lots of the former are easy to formalise and you can rely on the compiler to get it right. And that's what we are doing already anyway: even in C we just trust that a loop will compile to the appropriate conditional jumps and don't add defensive measures to check that.

Aaargh20318 9y ago
The point is that you're not going to do formal verification of your software. There is actually very little formally verified software out there, and the verified code that does exist is relatively small. And no, you can't rely on the compiler to get it right. Maybe if you only write Haskell you can get there 99% but there will always be human errors in code that the compiler can't find.
- eru 9y ago
  We rely on computers to get parts of our spec right all the time. Yes, a higher level language lets you offload more to the computer (like Haskell), but even in C we are doing some off that. Yes, in practice you seldom have much of a formal spec, agreed.