The ABI status of filesystem formats [LWN.net]

The ABI status of filesystem formats

Posted Oct 9, 2020 7:11 UTC (Fri) by bangert (subscriber, #28342)
In reply to: The ABI status of filesystem formats by NYKevin
Parent article: The ABI status of filesystem formats

A formal spec is not the panacea that one may be inclined to assume.

The way i see it, the only thing a formal spec does is to force upon (someone) to take ALL discussions about the subject of the article up front. That's practically impossible to get right and specifically when done well takes a huge amount of effort. If the developers were forced to do it, it would consume their time for a very long time - if someone else were to do it it would/could have a higher degree of defects.

You are highly likely to just debate the formal specification instead of the implementation.

While these objections apply to many situations the extra effort a formal spec introduces is worth it in (some|other) cases.

And although the conclusion of the article, that this subject will likely be discussed again, may be true, that is not in itself a bad thing (and the article does not say so).

to post comments

The ABI status of filesystem formats

Posted Oct 9, 2020 10:33 UTC (Fri) by roc (subscriber, #30627) [Link] (1 responses)

One nice thing about really formal specs (as opposed to careful English specs, which aren't really formal) is that for many specification languages you can find (or write) tools that leverage the specs to do useful work. For example, for a language like Alloy, fuzzing and model-checking tools can automatically generate testcases that are valid according to the spec and exercise all or most of the interesting edge cases (including many that the spec authors didn't think of).

You may also be able to prove useful consistency properties from the spec, e.g. that a "valid" filesystem doesn't have unaccounted-for blocks, etc.

The ABI status of filesystem formats

Posted Oct 9, 2020 10:35 UTC (Fri) by roc (subscriber, #30627) [Link]

What I meant to add was: if you write formal specifications the right way, you can use these tools to get more value out of the spec, which tilts the cost/benefit tradeoff towards formal specifications.

The ABI status of filesystem formats

Posted Oct 13, 2020 3:29 UTC (Tue) by marcH (subscriber, #57642) [Link]

> The way i see it, the only thing a formal spec does is to force upon (someone) to take ALL discussions about the subject of the article up front.

No, you can write a spec that formalizes an implementation. This is how most RFCs are written.