The design of a complicated system may proceed through many stages in its progress from specification to implementation. The correctness of the implementation should be established by subjecting each design decision to careful proof. This recommendation is illustrated by the first stage in the specification and design of a simple mail service. The fundamental theorem is that such a service can be implemented by a store-and-forward message passing switch, including both serial and concurrent links. The definitions and proof methods are those of a simplified trace model of Communicating Sequential Processes.