MIT develops file system with data guaranteed

Wired reports that MIT have used formal verification to write a file system that to probably will not lose data in the event of a crash. 

Making sure that the file system can recover from a crash at any point is tricky because there are so many different places that you could crash. You literally have to consider every instruction or every disk operation

They used Coq, a proof assistant that enabled them to build the system from the ground up in a logically consistent manner. 

Leave a comment

Filed under Programming

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.