The hard line on this is Dijkstra's "A discipline of programming", where he says, basically, that programming is hard and programmers should suffer. There's a case to be made for that, and it's the classic MIT programming philosophy.
Not everything needs to be done that way. Progress is made by encapsulating the parts that are really hard, so that second-raters can grind out appcrap fast enough to keep up with the market.
Problems come from exposure of hard problems at the higher levels. Race conditions at the application level tend to be poorly understood and handled badly. That's the sort of thing Lamport is addressing.
Any experienced engineer who tackles even a moderately complex coding problem and decides beforehand to think through that problem with a machine checked specification (say with Lamports TLA) will very likely discover that
1. His first 4, 5 attempts at the specification are not even close to being correct and his human mind was ill equipped to spot obvious problems without help.
2. The process of thinking through a such a spec focuses the mind precisely on what problem has to be solved and how to most economically address that problem -- neither of which he got right at the start.
3. The confidence in the implementation that follows the specification is far higher than the confidence he achieves through other typical methods (unit, human testing)
Thinking with a tool to help out may not be appropriate for every coding problem, but it does bring one to a very clear realization of how incredibly fallible one is in the face of complexity and the importance of thinking. And will cure you of statements like "having to think before you code isn't Agile" forever.
I had to check if you were being sarcastic: I believe not.
Ironically, Leslie focuses on precise thinking. Your central paragraph is a false dichotomy: it is incorrect to suggest that "programming being hard and/or programmers suffering" can't co-exist with "thinking before you code".
We all learn in different ways, and as people-who-sit-at-computers-to-make-them-do-stuff we are probably slightly more masochistic than the general population in a "school of hard knocks: learn it the hard way - by failing" sort of way.
However, a lot of us who are self-taught but have been working for a decade, two or more must follow a similar path: from just-code-and-suffer, through the experience of deep pain (particularly when maintaining such a beast for long periods), through finally to 'think twice, cut once' and an architectural focus as Leslie is getting at. His wisdom appeals to that acquired habit but specifically when considering new problem domains .. projects that unstructured thinking will have problems resolving to simple solutions, that solutions don't already exist for, and that are of a parallel and/or nontrivial nature.
His conclusion reminds me of the better vs worse popularity paradox. Maths are "simpler", but too strict, abstract and potentially cryptic. Many people will trade simplicity and power for ease of use even at the cost of complexity.
I believe it's easier for people to mentally conceive a machine looping over instructions than a transitive-closure or even an abstract fold.
Oh yes, this is not exclusive. As we like having many examples to understand a concept, we like to have things in many pieces, it helps us interact with it. In FP the set of ideas is so short and so abstract it ends up as an information ~vacuum. The other idioms let you assemble simpler less generic parts but at least it let's you acquire information, and that's something everybody likes.
Agreed: conceptual simplicity and therefore intelligibility at any given level of detail is a result of carefully designed and layered abstraction.
An important single-FP-language-codeball weakness is perhaps that of encouraging people to avoid clearly segregating these layers. Unix, by contrast, encourages a philosophy 'do one thing and do it well' for each smaller program, connecting them with simple interfaces, which arguably results in greater intelligibility.
You're not to come up with a simple design through any kind of coding techniques or any kind of programming language concepts. Simplicity has to be achieved above the code level before you get to the point which you worry about how you actually implement this thing in code. - Leslie Lamport
Law of Communications: The inevitable result of improved and enlarged communications between different levels in a hierarchy is a vastly increased area of misunderstanding.
The way I heard it, the SV office only existed in the first place because Lamport didn't want to move to Seattle. I kind of doubt they didn't offer him relocation, and I kind of doubt he accepted it.
The hard line on this is Dijkstra's "A discipline of programming", where he says, basically, that programming is hard and programmers should suffer. There's a case to be made for that, and it's the classic MIT programming philosophy. Not everything needs to be done that way. Progress is made by encapsulating the parts that are really hard, so that second-raters can grind out appcrap fast enough to keep up with the market.
Problems come from exposure of hard problems at the higher levels. Race conditions at the application level tend to be poorly understood and handled badly. That's the sort of thing Lamport is addressing.