I have no dog in this race, but... > the top-to-bottom branching is really jarring What do you mean? From what I've seen from skimming the first few chapters,

I have no dog in this race, but... > the top-to-bottom branching is really jarring What do you mean? From what I've seen from skimming the first few chapters, it uses 100% standard natural deduction proof trees. How would you present the proofs? (The "linear format" is indeed ugly, but it doesn't seem to be meant for human consumption.) > I've only seen it used in Type Theory and λ-calculus books That's the point of the Curry-Howard isomorphism: It's all the same thing. It makes sense to use the same notation.