da Tyga:

Thank you for writing back. I totally agree with your assessment. Permit me to elaborate a bit more on my situation.

I am a professional software engineer who is primarily dedicated to writing virtualization automation software for sales demonstrations. Naturally, our department is always interested in ways in which we can improve the efficiency of our virtualization environment(s). After reading 'L4 Virtualization and Beyond' (2008, http://os.inf.tu-dresden.de/papers_ps/haertig08_l4_virtualization_and_beyond.pdf), I became fascinated with L4.

I am here talking to you all because of the amount of press that seL4 has gotten as the proofed L4 kernel and because it appears to have the best, most easily understood documentation. Now, that does not mean that I think seL4 is well documented, just that it's the best documented of the L4 projects. The purpose of my original email was to very gently say that the introductory material to seL4 is so bad, that I'm willing to pay someone to either bring it up to date, assist me with it, or both.

For example, there is a thread about RefOS, wherein Kevin wrote, "RefOS was a student project that is now no longer actively maintained." Gapry and HyperNewbie, however, provided at least some fixes, but their fixes don't appear to have gotten any attention from upstream. This was on 11 February.

Nevertheless, RefOS appears to be the only seL4 project geared towards newcomers on the 'Getting Started' page (https://sel4.systems/Info/GettingStarted/). You should note that, on that page, there is no indicator that newcomers should, in fact, stay away from that project because it's no longer maintained.

I don't think requesting some attention on documentation is a bad or unjust thing. I would hope that lowering the barriers to entry to the seL4 community would increase the flow of developers, users, and sponsors to the seL4 project. In turn, I hope that would be seen as a good thing.

I'm offering part-time, albeit unofficial, company sponsored development in exchange for some paid tutoring. I am not asking for a hand-out. If I didn't have to worry about ramp-up time or coming up with deliverables, I wouldn't be bugging you.

Now, if you're worried about my qualifications, I'm a university educated computer scientist. While I've spent most of my career on web programming, I've studied operating systems development both at school and on my own. I began a toy kernel with the help of the osdev.org resources, and I'm happy with my progress. When I take inventory, however, I realize I don't have the desire to (re-)write an L4 kernel, nor do I think I can improve upon it.

Finally, I think you're referring to Professor Gernot Heiser's page at https://www.cse.unsw.edu.au/~gernot/, and probably more specifically the CS9242 course at http://www.cse.unsw.edu.au/~cs9242/current/. If you're referring to another course, please be more specific.

Thank you.

Andrew Jackman