On Wed, 26 Sep 2018 at 09:45, Chris Angelico email@example.com wrote:
On Wed, Sep 26, 2018 at 6:36 PM Paul Moore firstname.lastname@example.org wrote:
On Wed, 26 Sep 2018 at 06:41, Chris Angelico email@example.com wrote:
On Wed, Sep 26, 2018 at 2:47 PM Marko Ristin-Kaufmann firstname.lastname@example.org wrote:
- The contracts written in documentation as human text inevitably rot and they are much harder to maintain than automatically verified formal contracts.
Agreed, if contracts are automatically verified. But when runtime cost comes up, people suggest that contracts can be disabled in production code - which invalidates the "automatically verified" premise.
Even if they're only verified as a dedicated testing pass ("okay, let's run the unit tests, let's run the contract verifier, let's run the type checker, cool, we're good"), they're still better off than unchecked comments/documentation in terms of code rot.
Absolutely. But if the contracts are checked at runtime, they are precisely as good as tests - they will flag violations *in any circumstances you check*. That's great, but nothing new. I understood that one of the benefits of contracts was that it would handle cases that you *forgot* to test - like assertions do, in essence - and would need to be active in production (again, like assertions, if we assume we've not explicitly chosen to run with assertions disabled) to get that benefit.
There's certainly benefits for the "contracts as additional tests" viewpoint. But whenever that's proposed as what people understand by DbC, the response is "no, it's not like that at all". So going back to the "why isn't DbC more popular" question - because no-one can get a clear handle on whether they are "like tests" or "like assertions" or "something else" :-)