Any thoughts on a criticism of design by contract?

[amacfie]

@gabriel-fallen on Quora says

[...] To those who heard about “contracts”, “design-by-contract” (c) Bertrand Mayer and Eiffel, I’ve used that, I was part of research on that and I can tell you it doesn’t work. First of all class invariants are unsound and work only in simple cases. You have the whole bag of works with “callbacks”, mutual invariants (my invariant depends on invariant of another class) and so on. The formalisms to describe this — things like “object ownership” — are so complicated that they are unusable in practice and still forbid many use cases. Then to check pre- and postconditions you have to consider object reference aliasing which is an open problem yet. And again a complicated one. [...]

I'm curious if @pschanely, @mristin or others can comment on whether these statements have practical implications for people who use contracts or people who develop tools for contracts.

[mristin]

Hi, Unfortunately, I'm too busy at the moment. I'll come back to the thread with my thoughts after October 22nd.

[orsinium]

Hi, I'm a deal author and have a little bit of experience with DbC from both sides. There are my thoughts:

• I usually don't use class invariants. My usage of DbC is purely for contracts between functions. Partially, because of performance implications (deal validates pre-conditions on each setattr, getattr, and function call, which is a bit expensive by design). Partially, because the only place where you care about contracts is where you run some logic, the only difference is where you attach them.
• If your objects are immutable (typing.NamedTuple, dataclasses.dataclass(frozen=True), attr.s(frozen=True)), the only place where you need to validate the invariant is the constructor, which is also a function.
• Python type annotations system is also unsound. Using it you can do only a weak verification, and this is definitely better than nothing. If you need 100% formal verification, consider using Idris instead of Python because you need a language designed with it in mind. We (both Deal and CrossHair) try our best to attach formal verification on top of Python but it works only for some simple cases, just deal with it (pun intended).
• Hoare logic is sound, and the only thing you need for it are pre-conditions, post-conditions, and loop invariants. The latter also, in theory, can be straightened for most of the cases. Nothing about class invariants because they can be expressed by these three. You can read more on it in deal docs.
• In my understanding, object ownership matters mostly for concurrent code. In Python, I sometimes see issues with modifying mutable arguments in place but this is also possible to detect, and it's not so hard as it sounds. Currently, @sobolevn works on a type-aware linter, and I'm pretty sure we will be able to implement this check there (like "don't call list.append on passed arguments"). If you're interested in more powerful ownership control, it's also possible in theory, see capabilities in Pony language.

To summarize: don't worry about some corner cases when DbC maybe not sound. Sure, some bugs will slip through it. Still, you will catch most of the bugs, and this is bold. For example, deal has linter, test generation, formal verification, CrossHair integration (think as verifier-driven fuzzying), runtime checks. You write a few contracts and get all that stuff for free. Pretty cool, huh?

[gabriel-fallen]

A very nice summary, I pretty much agree with everything, thanks! 😃

One comment though.

In my understanding, object ownership matters mostly for concurrent code.

That's a misunderstanding, the problems arise even in single-threaded code. Rust community understands it very well, their favourite example is iterator invalidation: you can't modify a collection in the same loop you're iterating over it (with an iterator). That's my favourite example too, since I've got ConcurrentModificationException in a single-threaded code and was puzzled by it for a way too long of a time! 😄

[mristin]

Hi @amacfie ,
@orsinium already made a couple of points that I agree with. Let me try to re-iterate through the question once more and give you maybe a more practically oriented answer in addition to what @orsinium already said.

Call to authorithy.

Alexander Chichigin wrote:

To those who heard about “contracts”, “design-by-contract” (c) Bertrand Mayer and Eiffel, I’ve used that, I was part of research on that and I can tell you it doesn’t work.

This is a bit of a futile intro. I also worked and researched with Betrand Mayer (I was a teaching and research assistant with him at ETH Zurich), and I can tell you that it works. Perhaps the problem is with the expectations or a very fuzzy definition of what "works" (or "doesn't work", for that matter) means.

I did see contracts work in education. We had all our introductions to programming and software engineering classes with Eiffel. At least I haven't observed any issues (either as a student and among my co-students or as a teaching assistant).

I did see contracts work on larger code bases. We used contracts intensively at one of my previous employers (Parquery) for a code base of about 200-300K LOC. The code base grew ever since and they are still using it. You have to be careful which contracts are turned when (we distinguished levels: unit test, integration test, end-to-end test, production), but that requires only negligible attention in practice .

We caught quite some difficult bugs with contracts. For example, related to time conversions, edge cases in computer vision (e.g., image boundaries), out-of-sync caches and object properties (e.g., dictionary lookup over a list which always need to be in sync etc.).

Many tests did not have to be written, so it was also a nice plus for the code maintenance.

Expectations.

Alexander Chichigin wrote:

First of all class invariants are unsound and work only in simple cases. You have the whole bag of works with “callbacks”, mutual invariants (my invariant depends on invariant of another class) and so on. The formalisms to describe this — things like “object ownership” — are so complicated that they are unusable in practice and still forbid many use cases. Then to check pre- and postconditions you have to consider object reference aliasing which is an open problem yet. And again a complicated one.

I think this is a matter of expectations. I presume that Alexander Chichigin aims at very high correctness standards of the code. In that case, and I second what @orsinium said, contracts and conventional programming languages are not the appropriate tool.

On the other side, I do not see how he defines "simple" or why you shouldn't use contracts to cover the simple cases though you can not cover the "complex" ones. Contracts are such a low-hanging fruit that I hardly ever see substantial arguments against using them in the code. Most arguments cluster around people being not used to write them and/or being unwilling to put the minimal additional effort to formalize the contracts.

While I can not share companies' code, I can point you at the corpus of Python programs @pschanely, @LaurenDebruyn and I wrote and annotated with contracts: https://github.com/mristin/python-by-contract-corpus

Another good example that comes to my mind is a plug-in for Thonny I wrote: https://github.com/mristin/thonny-sealed. The development of that plug-in would have been much harder were it not for contracts.

Yet another example, though not in Python, is front end development with React and Redux where invariants can be neatly verified between each state update. For the example of that technique, see a simple game I wrote for my kids: https://github.com/mristin/bukvarko/blob/master/src/stateInvariants.ts

All these cases might indeed qualify as "simple". Judging by my personal experience, having contracts in place helped the development substantially, especially by catching some nasty bugs and being able to have deeper tests with much less explicit unit tests.

[gabriel-fallen]

Hi, @amacfie ! I'm kinda flattered you've found my old answer on Quora and traced me back to Github. 😊 Though I'm a bit saddened that you took my words out of context and used them as a background to pretty much irrelevant question. So to the question:

whether these statements have practical implications for people who use contracts or people who develop tools for contracts

No they don't.

The Quora question was about Dijkstra, so let me use another one of his quotes: "Tests can only show the presence of bugs but never their absence." (The quote isn't precise but the meaning is preserved.) That's obviously true, BUT. As exactly bug finding tool tests in general and contracts as a particular type of tests are indispensable and pretty efficient. Especially when combined with automation techniques like automatic test data generation (Property-Based Testing), fuzzing, mutation and so on. And as far as I can see this project does exactly that: it provides a tool to find bugs using Contracts and Automation.

So the bottom line is: my comments about contracts failing to provide absence-of-bugs guarantee are completely irrelevant for a project aimed at finding bugs.

And as a form of testing and partial static verification tool I personally a fan of contracts. I honestly believe it's better to have contracts than not, and encourage everyone to use them for their code. As well as tests and documentation. 😉 I was pretty disappointed contracts didn't make it into C# specification and were abandoned by Microsoft, they had pretty impressive and sophisticated work in that area.

Anyway, thanks for mentioning me in this project I'm pretty impressed by what the maintainers do here and will recommend it to my friends who are very into automated testing, contracts, PBT and fuzzing. 😃

[mristin]

Thanks for clarifications, @gabriel-fallen! I went to read the Quora post in full and would really like to moderate my original post and take back some of it's snarky tone. You are completely right, I misunderstood your quote without further context.

[amacfie]

Sorry @mristin, I had complete rather than partial verification on my mind at the time and I didn't even realize the context was important.

[gabriel-fallen]

@mristin no worries and no need to moderate your reply! I think you've done pretty detailed explanation and indeed figured out the context mismatch in terms of the difference between sound static functional verification (which contracts do not really provide, at least for complex industrial languages) and practical mixed static-dynamic approach to bug finding that you do.

And the "futile call to authority" is precisely correct characteristic of my quote. 😄 In the context of my Quora answer I decided to delimit the later opinionated and emotional part about contracts with that pathetic intro so readers would realize it's pathetic and opinionated and wouldn't take it too serious. Maybe I was wrong... 😅