Return

Crash Proof Filesystem

1 Name: Anonymous 2017-04-23 16:54
Using formal methods to verify a crash proof filesystem:

https://people.csail.mit.edu/nickolai/papers/chen-fscq.pdf
https://www.youtube.com/watch?v=fexr2IAJi_I

FSCQ is the first file system with a machine-checkable proof (using the Coq proof assistant) that its implementation meets its specification and whose specification includes crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ’s theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover the file system correctly without losing data.
2 Name: Anonymous 2017-06-28 01:41
crash proof motorcycle
3 Name: Anonymous 2017-07-01 00:41
>>2
That's called a car.
4 Name: Anonymous 2017-07-01 00:57
>>3
I thought it was a cdr.
5 Name: Anonymous 2017-07-05 11:51
>>4
It was a car.
6 Name: Anonymous 2017-07-06 03:40
/prog/ challenge: write a useful program + proof of its correctness, in coq
7 Name: Anonymous 2017-07-09 03:43
*with cock
8 Name: Anonymous 2017-10-14 15:54
What's the proof for Coq's correctness, i.e. that it never produces a false positive result?
9 Name: Anonymous 2017-10-14 21:24
>>8
there is none, and never will be (at least, not one which doesn't have the same problem), but i don't think that's so important - exploiting interpreter bugs to prove false generally is a very deliberate action, and proofs (to this point) are generally written by people who want, above all, to know that their own code is correct, and so are unlikely to take deliberate actions to prove their theorems using compiler bugs, not to mention the risk of being found out upon future interpreter updates (that might fix the bug they used to prove false). so i think that even if you can't prove coq correct, theorems proven in it are still very trustworthy, at least if they're not made by hostile entities (NSA writing a proof of a crypto implementation, for example)
10 Name: Anonymous 2017-12-09 03:52
prove your cock in my anus

Return
Name:
Leave this field blank: