The pioneering work of Hewitt and Baker on the foundations of concurrency during the seventies has inspired the development of the actor model as a promising object-based framework for understanding open distributed systems. So far, theoretical research on actors has focused on identifying the basic primitives of the model and on characterising the operational behaviour of distributed programming languages in terms of actor components. In this paper, we show that the actor model can also be used as a faithful basis for rigorously designing open distributed systems. We argue that a proof-theoretic approach is better suited to this purpose. An abstract-data-type-like axiomatisation of the actor primitives is proposed to support composing and reasoning from specifications of actor communities within a temporal logical system.