ทีมวิจัยจาก MIT เตรียมนำเสนอระบบไฟล์ที่ทนทานต่อความเสียหายหากคอมพิวเตอร์แครชไปในเวลาใดๆ ก็ตามระหว่างการเขียนไฟล์ ก่อนหน้านี้ระบบไฟล์มีการออกแบบเพื่อให้ทนทานต่อการแครชของคอมพิวเตอร์ ที่อาจจะหยุดทำงานไปบางเวลา หรืออาจจะไฟดับไปกลางคัน ทีมงานระบุว่าการออกแบบก่อนหน้านี้อาจจะทนทานต่อการแครชในเวลาใดๆ แต่ไม่เคยมีใครพิสูจน์จริงๆ ว่าหากมีการแครชระหว่างการทำงานช่วงที่ไม่คาดคิด จะมีบางช่วงที่ระบบไฟล์เสียหายได้หรือไม่ ทีมวิจัยอิมพลีเมนต์ระบบไฟล์นี้บนภาษา Coq ที่ใช้สำหรับการพิสูจน์ทางคณิตศาสตร์ โดยต้องนิยามบิตและดิสก์ขึ้นมา และนิยามความสัมพันธ์ว่าจะเกิดอะไรขึ้นหากระบบแครชไประหว่างการทำงาน จากนั้นจึงสร้างระบบไฟล์ที่พิสูจน์ทางคณิตศาสตร์ได้ว่าทนทานต่อการแครชในทุกช่วงเวลาทำงาน งานวิจัยนี้จะนำเสนอในงาน ACM Symposium on Operating Systems Principles เดือนตุลาคมนี้ ที่มา - MIT Mathematics, MIT, Research