I would present Lamport's thesis like this: engineering disciplines usually use a different formalism to reason about system from the one they use to construct it. Consider an electrical engineer designing an analog circuit, and a mechanical engineer designing a contraption made of gears, pulleys and springs. When reasoning about their designs, they can either use the “standard” mathematical approach, plugging in the equations describing what the components do, or invent an algebra of electronic components and an algebra of mechanical components and reason directly in a “language” of capcitors and resistors (one capacitor plus one resistor etc.) or a language of gears and springs. The engineers obviously use a domain-specific tool to design the low-level details of the system, but they use standard math to reason about it (to guide their high-level design and to make sure it achieves what they want). Lamport suggests that software engineers do the same.
In practice, most software engineers reason about designs only informally, and even then mostly in their heads. This is fine for simple things, but very hard to do when more complex software systems are concerned. The software verification (academic community) indeed uses an approach similar to Lamport (which uses more-or-less simple math to reason about programs), but they hide the techniques from the user, exposing them merely to the results in a sort of a CAD tool. The programming language theory community indeed tries to make mathematical reasoning explicit, but they're trying to make reasoning possible within the construction language (like the algebra of gears). There are a few advantages to that approach, but one major disadvantage: because programming languages, as Lamport notes, are so complex, the mathematics required to reason about them syntactically is very arcane and extremely complex; it is very much a completely new math. And because it is so new and so complex, PLT researchers have not yet been able to accomplish the task. Reasoning in that new math is currently much harder and much more limited that in Lamport's "simple math" approach[1]. Of course, it's possible that PLT will come up with good solutions in the future.
But in addition to the big pragmatic advantage of Lamport's approach (which may be temporary), he claims that using the universal language of "ordinary" math helps find the great similarities between different programs that can be written in many different ways, but are essentially the same. This helps to better understand what computation is, and also helps focus on the core issue -- how the program's environment behaves, how the program interacts with it, and why the program's behavior achieves its goals -- rather than being distracted right from the beginning by details such as the choice of abstractions (which are important only after the core issues are understood).
[1]: I sometimes see academic papers about how to reason about pretty basic program properties in Coq that would never be written about Lamport's TLA+ for the simple reason that an ordinary engineer would find them almost trivial in TLA+ after only a month or so since first encountering it.