Today I will be delivering a talk on the development and motivation behind the design of the language I am working on for the Trustworthy File Systems project at NICTA.

More information about FP-Syd, Sydney’s best functional programming user group, is available here. This month, we will (as usual) be hosted by Atlassian.

PDF of slides are available from here

Due to the sheer number of file systems a kernel needs to support, formally verifying a manually-written C implementation of each file system by hand is not a feasible approach to getting file systems verified. My project is about changing the implementation language for the file systems from C to a well-defined, controlled, domain specific language (CDSL) with a substructural type system that automatically establishes routine safety properties (e.g no undefined behaviour). From CDSL we aim to extract purely functional specifications of file system behaviour in Isabelle/HOL, an efficient C implementation of the file system, and a proof that shows that the C implementation is a refinement of the specification. Higher-level, filesytem- specific properties can then be manually proven on top of the generated specification. The end result is greatly reduced effort required to verify individual file systems, making verification of large numbers of file systems feasible. In this talk, I will discuss the design of this language, some of the problems I encountered when designing and implementing this language, and how the language fits into the overall context of our project.