The aim is to have a spec that is much LESS complex than the code, written at a higher level, abstracting away details. If the spec is 5x more complex than the code then indeed there’s no point.
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.
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.
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.