We argue that
— with public interfaces hiding private implementations — represent a form of
rather than ordinary data, and hence that proof methods for
programs are the appropriate techniques to use for reasoning with them. In particular, we show that the universal properties of unfold operators are perfectly suited for the task. We illustrate with solutions to two problems the solution to a problem in the recent literature.