To Lamport, and algorithm is an abstract mathematical concept. A computation is discrete dynamical system (analogous to a continuous dynamical system), which is generated by a machine (an algorithm), which expressed mathematically in a simple, almost-ordinary-math way, almost exactly like dynamical systems are expressed as ordinary differential equations. Reasoning is done entirely semantically (the syntax of Lamport's formalism isn't a programming language, and its semantics are simple mathematical semantics -- again, like ODEs).
Lamport's approach is best explained in the link I posted above (which is a very interesting read) and in section 6.3 of this paper (also an easy read, at least that section): http://research.microsoft.com/en-us/um/people/lamport/pubs/l...
In the conversation with Meijer, Lamport explains that he believes that "linguistic reasoning" 1. requires far more complicated math ("weird, computer science math", like domain theory, category theory, type theory etc.) but, in his opinion, that math doesn't really make reasoning about the algorithm any easier.
All I can say personally is that I find Lamport's view to be a more natural fit with how I think of algorithms (this is entirely subjective), and that learning his formalism to the level where you can specify and reason about very large, very complex real-world systems takes a "plain" engineer maybe two weeks of self study, while learning the more PL-based approaches to reach that level would take a programmer years. This is pretty objective. I can also say that I occasionally see academic papers that describe how to express and reason about some simple properties (like worst-case complexity) in Coq, which would be almost trivial for a TLA+ practitioner, no more than a month after first laying eyes on TLA+. So for me, at least, the difference is a pragmatic one.