[seL4] Re: SeL4 Source Code Documentation

On 20 Jun 2022, at 14:03, Isaac Beckett wrote:

Are those Haskell sources used to generate the C code, or are they an older version of the spec, or something? This is my first time hearing of them, so not sure what they’re used for.

The Haskell sources and spec are up to date (comments might not be). They are not used to generate the C code, instead the C code is proved to have the same behaviour as the those two. Just saw that Peter replied with the paper, I'd also recommend that one as an overview for how all this hangs together. Cheers, Gerwin