Modularity Matters Most

We contend that modularity is the key to improving software quality. We advocate a view of modularity that emphasizes not the mere assembling of software systems from component parts, but rather the specification of interfaces between components, verification that components meet their specifications, and the assembling only of components with compatible specifications. Key to this methodology is the use of types to specify and automatically to verify adherence to interfaces. We claim that this methodology makes a higher degree of software correctness possible than has often been achieved heretofore, and moreover, that it may be achieved in a practical manner. To reach this goal will require the development of sophisticated new type system, will require new techniques for modularizing certain correctness properties, and will require a delicate balance between concise code and automated checking.