The Rule of Maximum Practical Formality

At each step of a development, use descriptions that are as formal as possible.

This has two benefits:

  1. Formal descriptions are more precise than informal ones, which forces a thorough understanding of the issues and questions.
  2. More powerful verification methods for formal descriptions exist than methods for informal ones, so there is more confidence in each step’s correctness.

The rule of maximum practical formality was articulated in the paper Correctness by Construction: Developing a Commercial Secure System (see the top of page 21 and the bottom of page 19)