[qznc]

Here is a counter argument: http://www.pathsensitive.com/2018/10/book-review-philosophy-...

My summary would be: The spec must cover all possible implementations so it is usually larger than the most simple one.

An example from there:

> The authors of SibylFS tried to write down an exact description of the `open` interface. Their annotated version of the POSIX standard is over 3000 words. Not counting basic machinery, it took them over 200 lines to write down the properties of `open` in higher-order logic, and another 70 to give the interactions between open and close.

> For comparison, while it’s difficult to do the accounting for the size of a feature, their model implementation is a mere 40 lines.

[jacobr1]

How much of that is open/close being a poor abstraction, or overloading a bunch of semi-related functionality vs a more generalizable consideration systems designed with verification in mind.