Lamport argues that we should separate the "What?" from the "How?". I wonder though, for most problems, doesn't the "What" and the "How" of a program somewhat merge?
For example, are performance considerations part of the "What", or of the "How"?
For example, are performance considerations part of the "What", or of the "How"?
This is a huge mental error that people make over and over again. There is no absolute "what" and "how", they are just different levels of abstraction - with important inflection points along the way.
The highest level of abstraction is to simply increase happiness. Usually this is accomplished by trying to increase NPV. Let's do that by making and selling an accounting app. This continues to get more and more concrete down to decisions like "should I use a for loop or a while loop"
Clearly from the above example, "increase NPV" is not an important inflection point as it is undifferentiated and not concrete enough to make any difference. Similarly "for loop vs while loop" is likely not an inflection point either. Rather, there are important decisions along the way that make a given objective a success. Sometimes details can make a massive difference.
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!
However, a spec that has been sufficiently formalized (so that it can be executed) is an implementation. Maybe an implementation with certain (desirable or undesirable) characteristics, but still an implementation.
Of course there are informal, incomplete specifications that can't be executed. Those also have value of course, but I'd argue that writing those isn't programming.
Yes, the "hows" have impacts on performance. When implementing or selecting the "how" those performance criteria flow down into "how" requirements. As far as I am concerned that is no difference from correctness requirements placed on the "how".
Coming from the other direction. If I am hard disk manufacturer I don't care about the "what". I only care about the "how" of getting storage and the disk IO interface implemented so that my disk is usable by the file system abstraction that the "what" cares about. I may not know the exact performance criteria for your "what", but more performance equals more "whats" satisfied and willing to use my how.
Prolog by itself haven't found any real world applications as of today, because by ignoring the "How", performance suffers a lot, even though the algorithm might be correct.
That's the reason algorithms are implemented procedurally, and then some invariants of the program are proved on top of the procedural algorithm using a theorem prover like TLA+.
But in practice we implement procedural algorithms and we don't prove any property on top of them. It is not like the average programmer writes code for spaceships. The spaceship market is not significant enough to warrant that much additional effort.
The What puts constraints on the How, while the How puts constraints on the What.
I would say the the What is the spacial definition of the algorithm's potential data set, while the How is the temporal definition of the algorithm's potential execution path.