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.
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.
[+] [-] Animats|11 years ago|reply
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.
[+] [-] marco_salvatori|11 years ago|reply
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.
[+] [-] contingencies|11 years ago|reply
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.
[+] [-] agumonkey|11 years ago|reply
I believe it's easier for people to mentally conceive a machine looping over instructions than a transitive-closure or even an abstract fold.
[+] [-] contingencies|11 years ago|reply
[+] [-] amirmc|11 years ago|reply
In the SV office, which got shut down. I wonder if he's one of the few who got offered (and accepted) relocation.
[+] [-] Yawnoc2|11 years ago|reply