> 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 <[email protected]> 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ář <[email protected]> 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 >> [email protected] >> 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 > [email protected] > https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
