Hacker News Reader

True, but the same argument could've been made about the value of verifying the firmware. Eventually there will be enough formally verified pieces to put them together into a full software stack.

View on HN

Yeah.. but all the correctness in the world wont protect you from bitrot.

I think it's interesting, and would be great if something like this were applied to ZFS.

If under 'bitrot' you assume random bit flip here is the quote from that paper: << Project Zap [53,60] and Rely [8] explore using type sys- tems to mitigate transient faults (e.g., due to charged particles randomly flipping bits in a CPU) in cases when the system keeps executing after a fault occurs. These models consider possible faults at each step of a computation. The type system enables the programmer to reason about the results of running the program in the presence of faults, or to ensure that a program will correctly repeat its computation enough times to detect or mask faults. >>

That's a start, but not quite what I had in mind. I was more thinking of the case that you write 10001000, and then later, you read 10011000 back from the disk and the fs panics.

The words "checksum", "digest", or "integrity" don't appear in the paper at all.

It's probably a case of "in theory the bits you write to the disk are the bits you later read back, in practice they are not"

Reply on news.ycombinator.com