4 ms·

Pretty middlebrow dismissal. How about educating us about something pertinent to the paper in particular, instead of seemingly just scoffing at the idea of form

Pretty middlebrow dismissal. How about educating us about something pertinent to the paper in particular, instead of seemingly just scoffing at the idea of formal verification of software in general?

Natsu 11y ago
My comment was in no way intended as a dismissal of this work.
- throwaway999888 11y ago
  Those types of comments that lead off with a "by the way" of some witty quote has the effect of being dismissive in a pretty non-informative way. It's not that I think that's your intent at all; I have no doubts about your sincerity. Just telling you what effect it has, at least to my eyes. :)
  - Natsu 11y ago
    Well it's not that I can't see how someone could read it that way, that's why I edited in the disclaimer.
tokenrove 11y ago
It's pretty cool, but it's a little disappointing that they handwave away the possibility that block writes might not happen atomically. Formal verification is only as good as the assumptions you start from.
- anishathalye 11y ago
  I think it's more work to reason about partial block writes. The paper does have a paragraph on this: > The `disk_write` specification states that blocks are written atomically; that is, after a crash, a block must contain either the last-written value or one of the previous values, and partial block writes are not allowed. This is a common assumption made by file systems, as long as each block is exactly one sector, and we believe it matches the behavior of many disks in practice (modern disks often have 4 KB sectors). Using CHL, we could capture the notion of partial sector writes by specifying a more complicated crash condition, but the specification shown here matches the common assumption about atomic sector writes. We leave to future work the question of how to build a certified file system without that assumption.

4 ms·

Pretty middlebrow dismissal. How about educating us about something pertinent to the paper in particular, instead of seemingly just scoffing at the idea of form

by throwaway999888 11y ago

Pretty middlebrow dismissal. How about educating us about something pertinent to the paper in particular, instead of seemingly just scoffing at the idea of formal verification of software in general?

Natsu 11y ago
My comment was in no way intended as a dismissal of this work.
- throwaway999888 11y ago
  Those types of comments that lead off with a "by the way" of some witty quote has the effect of being dismissive in a pretty non-informative way. It's not that I think that's your intent at all; I have no doubts about your sincerity. Just telling you what effect it has, at least to my eyes. :)
  - Natsu 11y ago
    Well it's not that I can't see how someone could read it that way, that's why I edited in the disclaimer.
tokenrove 11y ago
It's pretty cool, but it's a little disappointing that they handwave away the possibility that block writes might not happen atomically. Formal verification is only as good as the assumptions you start from.
- anishathalye 11y ago
  I think it's more work to reason about partial block writes. The paper does have a paragraph on this: > The `disk_write` specification states that blocks are written atomically; that is, after a crash, a block must contain either the last-written value or one of the previous values, and partial block writes are not allowed. This is a common assumption made by file systems, as long as each block is exactly one sector, and we believe it matches the behavior of many disks in practice (modern disks often have 4 KB sectors). Using CHL, we could capture the notion of partial sector writes by specifying a more complicated crash condition, but the specification shown here matches the common assumption about atomic sector writes. We leave to future work the question of how to build a certified file system without that assumption.