Oh, that article is especially trollish, but there are articles like that in both camps.
> His alternative or-composition rule looks strange to me, since given either A or B it is entirely subsumed by simple implication, but his rule still seems to need both..?
It's not about "needing" both, but about how proofs are decomposed. Sometimes you need to prove `A ∨ B ⇒ C`; that's your proof goal. To do that, you prove `A ⇒ C` and `B ⇒ C`. That's all. If you look at basic texts about formal reasoning, they're full of such rules (see, e.g. https://en.wikipedia.org/wiki/Natural_deduction)
But from a pragmatic perspective, I think this is clear: if you want to formally reason about large, real-world programs today (especially if they're concurrent or distributed) "Lamport's" approach is the only affordable way to do it. It is also mathematically simple, very elegant and fun. Whatever you're interested in academically, it also covers the most important concepts anyway (refinement/abstraction relations, inductive invariance), and, in the end how you work and think is basically the same.