Reverse Mathematics is an on-going program of classifying mathematical theorems up to formal logical equivalence. The study has revealed a surprising degree of regularity. First, a large number of familiar theorems fall into a small number of equivalence classes. Second, these frequently occurring classes correspond to well-known classical programs in foundations of mathematics such as computable analysis (Pour-El/Richards), finitistic reducibility (Hilbert), predicativity (Weyl), and predicative reducibility. We survey the field and mention some old and new results and problems.