That's not what he means in that quote. He means that the extra work of decomposition (which can be done in either approach) is worth it if it's easier to use automated methods for each component separately. Those automated methods work equally well in both approaches (in practice, though, there is a production-quality model checker for TLA+, but not any that I'm aware of for "academic" programming languages). So your quote is completely orthogonal, and in any event, it is not the motivation for the "Milner approach".
There are several motivations for the PL approach: 1. an executable can be extracted from the code -- i.e., it can be compiled to an efficient program, 2. they believe that reasoning with syntax is easier, and 3. high-level reasoning could potentially assist in writing parts the program automatically. Lamport completely disagrees with point 2, and as to point 1, he says that had a language that could both reason about programs affordably and be compiled efficiently existed that would be great, but currently this is not the case. So he believes that they're sacrificing the simplicity of reasoning in a major way for the goal of having both programming and reasoning done in the same language. He may agree that it's a worthy goal, but one that we're currently far from attaining. He's interested in things that work on real-life software today. He says that how you program and how you reason about programs should not necessarily be the same, and if making them the same makes either of them significantly more complicated than would be possible when keeping them separate, then we should keep them separate.
There are several motivations for the PL approach: 1. an executable can be extracted from the code -- i.e., it can be compiled to an efficient program, 2. they believe that reasoning with syntax is easier, and 3. high-level reasoning could potentially assist in writing parts the program automatically. Lamport completely disagrees with point 2, and as to point 1, he says that had a language that could both reason about programs affordably and be compiled efficiently existed that would be great, but currently this is not the case. So he believes that they're sacrificing the simplicity of reasoning in a major way for the goal of having both programming and reasoning done in the same language. He may agree that it's a worthy goal, but one that we're currently far from attaining. He's interested in things that work on real-life software today. He says that how you program and how you reason about programs should not necessarily be the same, and if making them the same makes either of them significantly more complicated than would be possible when keeping them separate, then we should keep them separate.