Verifying non-functional properties of programs, such as time and/or energy consumption, is a difficult task. With applications such as the internet-of-things, it is becoming increasingly important that devices operate reliably \emph{within known time and energy bounds}. At the same time, processor architectures are becoming more complex. This means that traditional modelling techniques are not effective. Energy usage, for example, is \emph{non-compositional}. To solve this problem, we propose the introduction of type-directed, probabilistic bounds to allow us to reason formally about the approximate consumption of resources.