In this project we are interested in generating file system code for low-level file systems, those that run on specific media such as IDE and SCSI disks, CD-ROMs, floppies, MRAM, flash-memory devices, and more. The tool will take as inputs various parameters of the devices on which the file system needs to run (spinning magnetic media, random-access, etc.), system and user conditions (CPU and I/O parameters), desired features and layout of data (journalling, logging, extents, preallocated data, secure deletion, versioning, and many more). The tool will generate code for a file system plus user-level tools that can be used to format, backup, and verify the file system. The benefits of such a tool and a high-level language are that it can generate optimal code for the specific file system, prove that the code is correct (avoid coding mistakes), and even be able to migrate the file system's on-media format to another format.
Of particular interest to us is the ability to produce file systems for constrained environments such as mobile devices, where there may not be an MMU, space is small, outside connectivity is unreliable and slow, and power consumption is at a premium.