> Rarely do I encounter a program whose problems are in their essential complexity. I'm not saying we don't also introduce non-essential complexity, but I thi

> Rarely do I encounter a program whose problems are in their essential complexity. I'm not saying we don't also introduce non-essential complexity, but I think that working on distributed/interactive/concurrent systems and specifying them in TLA+, which allows us to expresses just essential complexity, will dissuade you of that notion. Because TLA+ allows you to either write a proof of an assertion or to automatically look for counterexamples with a model checker, it makes it easy to compare the relative difficulty of those two activities. Not only is proving much harder, in most cases you'll find that "intuitive" reasoning is just wrong.