Program decomposition into modules

The quality of a program has many aspects and is an elusive property. A user of a program may judge it according to its efficiency, reliability, or convenience of user dialog. Whereas efficiency can be expressed in terms of numbers, convenience of usage is rather a matter of personal judgement, and all too often a program’s usage is called convenient as long as it is conventional. An engineer of a program may judge its quality according to its clarity and perspicuity, again rather elusive and subjective properties. However, if a property cannot be expressed in terms of precise numbers, this is no reason for classifying it as irrelevant. In fact, program clarity is enormously important, and to demonstrate (prove?) a program’s correctness is ultimately a matter of convincing a person that the program is trustworthy. How can we approach this goal? After all, complicated tasks usually do inherently require complex algorithms, and this implies a myriad of details. And the details are the jungle in which the devil hides.