Dmytro Taranovsky has a Web page on which he claims to define a system of ordinal notations strong enough to provide an ordinal analysis of full second-order arithmetic. I think (perhaps unjustly) that this claim is suspicious, since from my passing acquaintance with the subject I seem to understand that the state of the art of ordinal analysis was around $\Pi^1_2$-comprehension (e.g., Jan-Carl Stegert's doctoral dissertation building on work by Michael Rathjen), the ordinal notation systems involved are considerably more complex (reflection instances, collapsing hierarchies), and Taranovsky mentions none of this. On the other hand, a superficial look at his page *does* seem to make some kind of sense, and my interest in the subject is to choose the largest possible system of ordinal notations which isn't too fastidious to implement on a computer (i.e., I'm not concerned with the proof-theoretic aspect).

So before I decide to read it in great detail or not, I'd like an expert's opinion: what is to be thought of Taranovsky's ordinal notation systems? (Might they define an ordinal which is not as large as claimed? Or perhaps which could be as claimed but would be very difficult to analyse?)