Re: [seL4] FYI: microkernel.info community site

Interesting statement on the Muen kernel section: "The world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. “

We proved full functional correctness (which is a superset of absence of runtime errors) for seL4 in 2009. I must be missing something.

I believe how it is meant is the following: "The first kernel to both reach being open source and being proven to contain no runtime errors is Muen." (of course among the kernels that are *now* open source, seL4 is the first one for which the absence of runtime errors was proven) Wolfgang On Thu, Mar 10, 2016 at 10:33 PM, Gernot Heiser wrote:

Interesting statement on the Muen kernel section: "The world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. “

We proved full functional correctness (which is a superset of absence of runtime errors) for seL4 in 2009. I must be missing something.

Gernot

...

On 11 Mar 2016, at 6:50 , Jakub Jermář wrote:

Hello,

just FYI, I have set up a simple web page[1] to promote the wider microkernel community and its goals. So far, the page comes with a brief description of the microkernel concept and an incomplete list of microkernel projects with links to each project's web. The description is made out of the first two sentences I found in the "What is XYZ" section or elsewhere on the web of the respective project. I also took the freedom to use the respective project's logo (or what I believed was the project's logo) for promoting it.

I hope you will find this small web a good idea. It was inspired by a similar (though a little bit more informative) site set up by the unikernel community [2]. The sources of the [1] web are hosted on Github [3], so feel free to submit issues or PR to make the site better.

Please send me a PM if there are any issues pertaining your project's cartouche that cannot be dealt with using Github.

Thanks, Jakub

[1] http://microkernel.info [2] http://unikernel.org/projects/ [3] https://github.com/jermar/microkernel.info

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel