I think he argues that more thought should go into explicitly designing the behaviour of a software system ("What?"), independently from its implementation ("Ho

I think he argues that more thought should go into explicitly designing the behaviour of a software system ("What?"), independently from its implementation ("How?"). Explicitly designed program behaviour is an abstraction (an algorithm or a set of rules) separate from its implementation (code written in a specific language). Even if a user cannot precisely explain what a program needs to do, programmers should still explicitly design its behaviour. The benefit, he argues, is that having this explicit design enables you to verify whether the implementation is actually correct. Real-world programs without such designs, he jokes, are by definition bug-free, because without a design you can't determine if certain behaviour is intentional or a bug. Although I have no experience with TLA+ (which he designed for this purpose in the context of concurrency), this advice does ring true. I have mentored countless programmers, and I've observed that many (junior) programmers see program behaviour as an unintentional consequence of their code, rather than as deliberate choices made before or during programming. They often do not worry about "corner cases", accepting whichever behaviour emerges from their implementation. Lamport says: no, all behaviour must be intentional. Furthermore, he argues that if you properly design the intended program behaviour, your implementation becomes much simpler. I fully agree!