We at Galois are quite interested in formally verified software. An OS would be very exciting.
We have offered Halfs, a Haskell filesystem, and would be delighted if someone worked to formally verify this. As the primary author, I'd be happy to tweak the Halfs code to make it easier for someone working to verify it. http://www.haskell.org/halfs peace, isaac _______________________________________________ Haskell mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell
