[mdaniel]

> In an ideal world, you'd nail your FS design first try, make no mistakes during implementation and call it a day

Crypto implementations and FS implementations strike me as the ideal audience for actually investing the mental energy in the healthy ecosystem we have of modeling and correctness verification systems

Now, I readily admit that I could be talking out of my ass, given that I've not tried to use those verification systems in anger, as I am not in the crypto (or FS) authoring space but AWS uses formal verification for their ... fork? ... of BoringSSL et al https://github.com/awslabs/aws-lc-verification#aws-libcrypto...

[orbital-decay]

A major chunk of storage reliability is all these weird and unexpected failure modes and edge cases which are not possible to prepare for, let alone write fixed specs for. Software correctness assumes the underlying system behaves correctly and stays fixed, which is not the case. You can't trust the hardware and the systems are too diverse - this is the worst case for formal verification.