I'm pretty familiar with this notation. No, he isn't trolling, it's not a practical joke, and even though it might seem esoteric and trivial to the outside world (hell, what academic disciple isn't?), he has a good point. The foundations of programming languages should use a consistent notation with well-defined semantics. Of course, theorem provers can encode most of these kinds of rule systems, and do have a concrete syntax that is not nearly as concise, but they do force the formalism into an automatic checker. Some academics really hate the "programming" of using a theorem prover, but I find it to be an incredible boon to the field.