@LSpice (missed your reply, so over 3ys later...) - The most important example: set-off or vertical lists (e.g., bullet points) - if you turn "There were three things in the basket: an old newspaper, a loaf of bread, and a rusty knife." into a Chicago-style vertical list (per CMoS 16th, 6.124), the only punctuation mark you will keep is the colon. I should not have downvoted Mariano's answer - the reasoning might be unsound, but it is commonly given and deserves to be documented.

Not quite: you need an axiom to do non-inductive case reasoning on naturals in Q.

The really big observable benefit with microtypography is less hyphenation.