In his influential 1981 « green » book, Gromov introduced a notion of distance between compact metric spaces and established a foundational compactness theorem for the space of metric spaces. When applied to certain classes of smooth Riemannian manifolds, this theorem yields a precompactness result, allowing the extraction of subsequences of smooth Riemannian manifolds degenerating into singular metric spaces. I will discuss how this result has shaped modern geometric analysis, highlighting kew example