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..? Or am I missing something about his notation?
Section 6.3 also contains unsubstantiated claims about what is "popular among computer scientists" and what "many computer scientist" do or that they "denigrate the use of ordinary mathematics". I mean, this guy knows who he is talking about, why not call them out on the specifics? (He does reference one paper, and then attacks it by comparing it to a specification he worked on, which he does not reference.)
He's obviously way smarter than me, and I think I understand his general position, but it's hard to get at his arguments when he wraps them in some much hostility.
Personally I'm more interested and fascinated by the stuff going on in the Milner camp, so I'm obviously biased against him. But I do think the most fruitful approach is to have many people working in different directions and seeing what falls out, instead of trying to prove a priori that a research direction is useless.