The Multiple Birkhoff Recurrence theorem by Furstenberg and Weiss in 1978 is a seminal result for the interaction between topological dynamics and combinatorics, establishing Ramsey-type theorems through corresponding recurrence results. However, while combinatorial proofs often contain explicit quantitative information, topological proofs usually do not contain realizers, bounds or similar data. EG for van der Waerden's theorem -- for every finite colouring of the integers one colour contains arbitrarily long arithmetic progressions -- one may ask for a number N = N(q; k) such that for every q-colouring of [0;N] one colour contains a progression of length k. The combinatorial proof contains an explicit upper bound on N(q; k), while Furstenberg and Weiss' topological proof does not. Thus one may ask: what is the algorithmic content of the topological proofs of Ramsey-type theorems? We will present an analysis of Furstenberg and Weiss' Multiple Birkhoff Recurrence theorem which generalizes a previous analysis by Girard. We will also discuss the use of compactness in proofs of the Multiple Birkhoff Recurrence theorem, IE the concept of minimality in topological dynamics, sketch the treatment of generalizations of the Multiple Birkhoff Recurrence theorem, and, if time permits, survey some related proof mining results in ergodic theory.