We establish a rigorous bridge between two historically distinct routes to Haar measure: the classical topological route (locally compact groups) and a measure-theoretic route (measurable groups via projective limits of finite groups). We prove the Halmos–Weil theorem from first principles: a separated measurable group with separable measure algebra carries a canonical Weil topology making it a compact, second-countable topological group whose Haar measure coincides with the original one. We determine the exact boundary between the two routes: countable projective limits of finite groups yield metrizable profinite groups; uncountable limits diverge precisely through non-separability of the measure algebra (Maharam type ≥ ℵ₀). We present complete, self-contained proofs of existence and uniqueness of Haar measure, of the extended Daniell–Kolmogorov theorem, and of the Halmos–Weil theorem. We develop three applications: random-order values for non-atomic games (with full axiomatic characterization and uniqueness), invariant statistical decision theory on general (non-compact, non-unimodular) groups, and Haar measure as the canonical reference for Lie-group generative models. All numerical illustrations are executed and verified.