Cutting planes were introduced in 1958 by Gomory in order to solve integer linear optimization problems. Since then, they have received a lot of interest, not only in mathematical optimization, but also in logic and complexity theory. In this paper, we present some recent results on cutting planes at the interface of logic and optimization. Main emphasis is on the length and the rank of cutting plane proofs based on the Gomory-Chvátal rounding principle.