Capabilities are increasingly used to reason informally about the properties of secure systems. Can capabilities also aid in formal reasoning? To answer this question, we examine a calculus that uses effects to capture resource use and extend it with a rule that captures the essence of capability-based reasoning. We demonstrate that capabilities provide a way to reason for free about effects: we can bound the effects of an expression based on the capabilities to which it has access. This reasoning is ``free'' in that it relies only on type-checking (not effect-checking); does not require the programmer to add effect annotations within the expression; nor does it require the expression to be analysed for its effects. Our result sheds light on the essence of what capabilities provide and suggests useful ways of integrating lightweight capability-based reasoning into languages.

In this OCAP 2017 talk we will describe our progress on effect inference and how it can benefit from capabilities as well as discuss our later work on polymorphic effect inference.

NB! This paper is a cut down version of our larger publication under consideration for another ACM conference and thus will not be published but only presented at the workshop for the discussion purposes.