Roughly speaking, a measure on a metric space is porous if every ball around a typical point contains a measure-theoretic ``hole'', i.e. a ball of comparable size but much smaller measure. A measure is mean porous if for almost every point there is a positive proportion of scales at which the measure is porous (in other words, not all balls contain a hole, but balls of many radii do). It seems intuitively clear that a porous measure, and even a mean porous measure, may not have full dimension. A sharp rigorous version of this was stated by Beliaev and Smirnov in 2002, but their proof is incorrect. I will present a complete proof of their statement, which is based on a probabilistic/dynamical approach to computing dimension.