Separating the "What" from the "How" is a pretty old idea originating from Prolog, and yes you can do that. Erlang for example, in which many of Lamport's ideas

Separating the "What" from the "How" is a pretty old idea originating from Prolog, and yes you can do that. Erlang for example, in which many of Lamport's ideas are implemented, is a variation of Prolog. 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.