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.
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.
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.