Halfs is a filesystem implemented in the functional programming language Haskell. Halfs can be mounted and used like any other Linux filesystem, or used as a library. Halfs is a fork (and a port) of the filesystem developed by Galois Connections. We've created a virtual machine to make using Halfs extremely easy. You don't need an extra partition or a thumb drive, or even Linux (Windows and Mac OS can emulate the virtual machine). For the impatient, go to the quick start: http://hackage.haskell.org/trac/halfs/wiki/QuickStart The Halfs web page is here: http://www.haskell.org/halfs/ Background: In the course of developing a web server for an embedded operating system, Galois Connections had need of a filesystem which was small enough to alter to our needs and written in a high-level language so that we could show certain high assurance properties about its behavior. Since we had already ported the Haskell runtime to this operating system, Haskell was the obvious language of choice. Halfs is a port of our filesystem to Linux, with some modifications. High assurance development is a methodology for creating software systems that meet rigorously-defined specifications with a high degree of confidence. That methodology comprises tools and practices. Its goal is to produce such systems reliably and effectively, with an ordinary degree of developer effort. Haskell is particularly well-suited to high assurance development. It is a high-level, fully-expressive, pure, functional language, with a powerful type system. One of the obligations of high assurance development is the demonstration of strong correspondence between high-level executable models and the eventual implementation. Haskell supports this directly: it can describe systems all the way from high-level executable models through to system implementations. The fact that Haskell is pure comes from its mathematical basis, and means that, by default, a function does not interfere with other functions. The type system is an automatic and scalable proof engine that can encode and enforce desirable properties. Together, these features allow the correctness of complex systems to be established, making Haskell ideal for high assurance development. The question was whether Haskell is well suited as the implementation language for a filesystem, which involves fixed sized buffers, lots of IO, and binary data structures. Though correctness is much more important to us than performance, we hoped that a Haskell filesystem would have acceptable performance, and that writing such low-level code would not be awkward or error-prone. We have developed a filesystem, Halfs, which aims to answer the above questions. One may mount a Halfs filesystem in Linux using the FUSE (Filesystem in Userspace) kernel module. We have created two new monads, FSRead and FSWrite which restrict the IO monad to reading and writing operations respectively. For performance, Halfs uses efficient mutable arrays for block IO, as well as caching for blocks and inodes.