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