Mezzo is (a proposal for) a programming language equipped with an expressive type-and-permission system. Like ML, it is a high-level programming language, equipped with algebraic data types, first-class functions, polymorphism, garbage collection, etc. Its main innovation, in comparison with ML, is its affine type-and-permission system, which does not just describe the structure of data, but controls who has permission to read or write, and allows types (and permissions) to evolve over time. In this talk, I would like to give an informal overview of Mezzo's main design principles, followed with a more technical look at Mezzo's metatheory. The proof of type soundness, which has been verified in Coq, is first carried out for a core affine lambda-calculus, then extended with three independent features, namely affine references, locks, and adoption-and-abandon.