COGENT: A linearly typed programming language for verified systems code

Toby Murray (University of Melbourne)

Toby Murray (Melbourne) will give a talk titled "COGENT: A linearly typed programming language for verified systems code". 

Abstract: Systems code underpins the safety and security of many critical systems, yet is predominantly written in unsafe languages like C and C++, whose unwieldy semantics make verifying code correctness incredibly effort-intensive.

In this talk we present the COGENT programming language, a restricted,
polymorphic, higher-order, and purely functional language with linear
types and without the need for a trusted runtime or garbage collector.
Linear types allow us to assign two equivalent semantics to the
language: one imperative, suitable for efficient C code generation; and
one functional, suitable for equational reasoning and verification.
We discuss our experience using COGENT to build two Linux file systems
and to verify functional correctness properties of one of them.
Experience to date suggests that verifying COGENT code is significantly
easier than for traditional systems code verification, like the seL4
project to which we compare.