I don't have anything in particular to contribute, but it struck me as interesting that the term private understanding is used here. It reminds me of the subtitle of one of the more well-known books on formal methods, The B-Book: Assigning Programs to Meanings. [0]

Of course, using a formal methodology like B, ceaseless, flawless vigilance is mandatory.

[0] https://www.cambridge.org/gb/academic/subjects/computer-scie...