At Trustworthy Systems, we are one of the few places that understand software verification. We’ve built the worlds only verified, general purpose micro-kernel. And many people in the group are core contributors to Isabelle/HOL and CakeML. And, as a group, we not only believe in software verification, we understand what it involves, and also realise that the returns we get from verified software don’t come cheap. With that in mind, we started working on Cogent, with the aim of reducing the cost of verified systems. For those who are keen to read about how we achieve that, I suggest reading the publications section here.
What is Cogent?
Cogent is a restricted, polymorphic, higher-order and purely functional language with linear types and without the need for a trusted runtime or garbage collector.
In the context of Cogent, the adjectives that I used above, mean the following:
- restricted: Cogent omits certain features that one might come to expect from a programming language. For instance, Cogent doesn’t support general recursion.
- polymorphic: This is similar to templates in C++ or generics in Rust.
- higher-order: Cogent uses software components like functions, modules or objects as values.
- purely functional: Cogent forbids changing state, mutable data. Evaluation is done similar to a mathematical function.
- linear types: ‘Objects'(although there is no such concept in Cogent, I’m using it to very broadly define instances/variable of a particular type) can be used exactly once. Rust does something similar, I think.
- trusted runtime: Cogent compiler generates C code, so the trusted component is limited to the C runtime system.
- garbage collector: Since Cogent compiler generates C code, we would manage memory manually, like we do in any C program.
Being very new to functional programming, language theory and type systems, my level of understanding of the theory behind the earlier mentioned concepts, is still pretty shallow. For an authoritative and in-depth explanation of these concepts, please refer to the Cogent publication list and Liam O’Connor‘s(one of the compiler writers, the other being Zilin Chen) blog, where he occasionally writes about the compiler and type system.
As mentioned earlier, one of the key ideas behind developing Cogent is to reduce the cost of verifying software. Since we are a systems engineering research group, our focus is particularly on reducing the cost of verifing system software. And that brings us to the next key question.
What can Cogent be used for?
I want to respond to the question with the answer, “For anything”, but I would be lying. If you intend to write a program in Cogent that prints a “Hello, World”, I can tell you that it isn’t possible without using C code, since we don’t have IO support in Cogent. Infact things that are simple to write in other programming languages, loops for example, have very complicated usage patterns in Cogent.
I think, for any compiler to be good enough, it takes a long time and a lot of man-years(Look at gcc, llvm/clang, rustc and various other mature compilers). In comparison, Cogent is still in its infancy and at our peak, we had about 4 compiler developers(We have 2 people working on the compiler now). Having said that, the Cogent compiler does let us write verifiable Linux file system drivers, and it does some parts of it well. Infact we have implemented 3 filesystems(at various levels of completion) in Cogent – bilbyfs, ext2 and vfat. All of the Cogent source is available on Github.
Our eventual goal is to have complete implementations of these(and more) filesystems along with other parts of the system software stack, viz., networking code, drivers and the like. Currently the implementations we have in Cogent have varying degrees of performance costs(based on the usage, as highlighted in the Cogent paper), but we are working towards making sure that we don’t lose out on performance, although we aren’t there yet.
Why?
I’ve already explained why we are working on Cogent, and what our goals are. And if I have piqued your interest enough, I suggest that you got read some of the papers in the publication list.
What I want to mention is why I’m writing about this now. Two reasons. One, I think writing about it will give me a lot more clarity about what I’ve personally done so far, and what I want to do with the project going forward. And two, I want to be able to talk about Cogent from an engineers perspective. When I started working on this project a year ago, I was overwhelmed. Having mostly used imperative languages for as long as I remember and having primarily done systems programming, everything looked daunting. It was a steep learning curve trying to understand functional programming, Haskell, software verification. And after having spent a year trying to implement ext2, f2fs and contributing a little to the compiler, which is written in Haskell(I forgot to mention that earlier), I’ve started to appreciate these ideas a lot more. I have barely scratched the surface, but I’m very enthusiastically digging deeper.
My idea is to write several posts about using Cogent and this post is meant to be a curtain-raiser for the posts(time permitting) that follow.
One last thing. Liam gave a talk titled, Refinement through Restraint: Bringing Down the Cost of Verification at ICFP 2016, the video of which is available here. The 26 minute talk is both entertaining and informative and it is worth a watch.
Partha Susarla 