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.