Proof mining (which even has a short [Wikipedia article](https://en.wikipedia.org/wiki/Proof_mining)!), and area in large part developed by Kohlenbach, is mentioned briefly in the comments, and I thought it deserves a bigger mention. Roughly speaking, proof mining is the idea that from non-constructive proofs of existence one can often extract effective bounds. For example, from the standard proof of the irrationality of $\sqrt{2}$ it is not hard to show that for any irreducible rational $\frac{a}{b} \neq 1$ we must have that $|\frac{a}{b} - \sqrt{2}| > \frac{1}{2b^2}$ (try it yourself!). This ties in with the [irrationality measure](https://en.wikipedia.org/wiki/Liouville_number#Irrationality_measure) of a real number.  

Especially in its applications to functional analysis, such as in [Kohlenbach, U.; Leuştean, L.; Nicolae, A.; *Quantitative results on Fejér monotone sequences*. Commun. Contemp. Math. 20 (2018), no. 2], proof mining really shines through as a powerful set of techniques.

I attended a summer school in 2016 in which Kohlenbach presented [these slides](https://www.uni-goettingen.de/de/document/download/ae21de540e6a9ea9bb66009f4cb1c81b.pdf/Kohlenbach-slides.pdf) -- they are a gold mine of information, but can be rather dense at times. However, they provide an excellent overview for many important concepts in the area (such as Herbrand normal forms) and highlight many applications. A good introductory text is also [this text by Kohlenbach and Oliva](https://www2.mathematik.tu-darmstadt.de/~kohlenbach/novikov.pdf).