1. Things that I feel I could easily reconstruct given just the end result and enough time, because really, I understand what ordered logic ought to be, and much of it plays out just like you'd expect. Pleasantly routine — to put it an even nicer way, canonical-seeming — properties and proofs. These things make me feel all smart and stuff. Examples: basic logic and type theory, and the uniform proof system.
2. Things that I feel I could reconstruct, but god it would be so annoying, because we have better technology now. These things make me feel immensely grateful for the collateral inventions that came along with the development CLF, by which I mean I am immensely grateful for something I like to call "Kevin Watkins". Examples: tedious decidability proofs, logical relations arguments, type conversion rules, and the gaping chasm between the definitional and algorithmic systems.
3. Things that perplex me so much I don't understand what it is I don't understand. Coupla chapters like this. Things like how he handles the nondeterminism peculiar to the ordered system, because when you pick an unrestricted or mobile formula to copy and focus on, you have to decide where in the ordered context it shows up.
4. Delicious examples of ordered logic programs. I hope to cook up some way of handling their metatheory in my framework, but yikes it looks hard right now.