There are several ways to strengthen the notion of well-foundedness for orders that are not total. A particularly intriguing choice is the notion of better-quasi-ordering (bqo) due to C. Nash-Williams, which became instrumental in R. Laver's proof of Fraïssé's conjecture. From the viewpoint of reverse mathematics, the theory of bqos depends on unusually strong axioms: even the statement that all finite orders are bqo requires at least arithmetical recursion along the natural numbers (which is the same as omega-th Turing jumps; the resulting theory is denoted ACA_0^+). Perhaps surprisingly, the only known proof of this result makes essential use of ordinal analysis. Indeed, G. Gentzen's archetypical result that Peano arithmetic (PA) has proof-theoretic ordinal epsilon_0 is still visible in the analysis of finite bqos. In the course, I will introduce bqos, recall the ordinal analysis of PA, and show how the two come together to produce the aforementioned result about finite orders.