In contrast to spin system taking value in a finite group, those invariant under the action of the rotation group SO(2) never have an ordered phase in if the lattice is 2-dimensional. So what does happen? In the sixties, physicist Berezinskii, Kosterlitz and Thouless predicted that a more subtle phase transition should appear if the spins are abelian; in terms of the two-point functions this manifests itself as a transition between exponential decay and power-law behavior. The transition is now called the BKT transition. In the late eighties Fröhlich and Spencer famously provided a rigorous proof of such a transition in the planar XY model. In the talk, I will introduce a loop representation of the XY model which allows to transfer information between the model itself and its dual height function. I will use the link to give a new proof of the BKT transition. The loop representation can also be used to provide simple proofs of correlation inequalities. Based on joint work with Marcin Lis.