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:

WordPress.com Logo

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

Twitter picture

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

Facebook photo

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

Google+ photo

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

Connecting to %s