Re: Fwd: seL4 is going open source
"Jonathan S. Shapiro" <[email protected]>
| Newsgroups | gmane.comp.capabilities.general |
|---|---|
| Message-ID | <CAAP=3QOOSaezdNggOTZQtvP81ULGKUwGZVoT4pe9SK_8giiAtg@mail.gmail.com> |
I'm pleased to see the open source announcement for seL4, but I have mixed feelings about it. I think it's worth noting that: 1. OKL4 actually *was* open source until OKLabs took it proprietary. That doesn't make me feel warm and fuzzy. 2. So far as I know, seL4 isn't a kernel that is actually shipping. Regardless, I'm delighted to be able to openly examine how NICTA/OKLabs approached the formalization and verification process. I'll be interested to see if the formalization errors that we have identified in some prior work have been addressed. Given the reticence with which the group has reacted to questions and issues raised by Scott Doerrie and myself, it will be good to be able to carefully examine and review the work. No proof is perfect. The ability to explore their approach in depth is *very* valuable. Jonathan _______________________________________________ cap-talk mailing list [email protected] http://www.eros-os.org/mailman/listinfo/cap-talk