On Consistency: A Response to "Response to 'Response to "Ramen, Beans, and Potatoes, Oh My!"'"

The only way to find an error is to compare two different things. In software engineering, the two things are often the behavior of a program and the intended behavior of the program.

For example, testing finds errors by using the test suite as the intended behavior. In the worst case, the intended behavior exists only in the mind of the developer, and finding errors involves comparing the developer’s mental model to the source code or observable behavior of the program. If the intended behavior is captured in a requirements document or in code comments, then developers also manually compare the intended with the actual behavior. In the best case, the intended behavior is formally specified. A developer then constructs a proof (typically with machine assistance) that the program satisfies its specification.

Programmers are often resistant to do their job twice: once to specify behavior, and once to implement behavior. When the two things match, comparing them yields no new information, and it may seem that the extra effort was wasted. The specification has no effect on the run-time behavior of the code, which is what the customer cares about. A similar argument applies to writing types in a program: they are redundant with the program operations. Nonetheless, I like to write types at interface boundaries, such as on procedure signatures, because they localize type errors and they serve as valuable documentation of my intent.

This discussion reveals a key weakness of automatically creating tests, types, or specifications: when they are inferred from a program, they are not an independent artifact. They are merely a re-statement of the program. This means that comparing an inferred specification to the program is not an effective way to find deep errors. However, these inferred specifications have great value in a different sense. You can compare different parts of the inferred specification to one another. If the inferred specifications of a caller and a callee are inconsistent, you have found a problem.

James’s thoughtful blog post points out the critical importance of consistency across parts of a system, and it shows what problems inconsistency can cause. Not only must the parts be consistent, but the measurements should be commensurate. This suggests a way to solve all the problems: the world should consistently use the simple and intuitive imperial system of measurements rather than the messy, confusing, newfangled metric system.