Hi, See our active discussions at comp.micro-kernel.l4.devel:
http://thread.gmane.org/gmane.comp.micro-kernel.l4.devel/2030 Thanks Shams -- "Jonathan S. Shapiro" <> wrote in message news:[EMAIL PROTECTED] > On Fri, 2007-06-08 at 09:19 +0530, Prem Mallappa wrote: >> > [1] http://ertos.nicta.com.au/research/sel4/ >> >> Looks like it is written in Haskell, anybody has/interested in 'C/C++' >> implementation? > > This is not quite what is happening. The seL4 project has built an > executable *model* of the system in Haskell. This version is a complete > but unoptimized version of seL4. It runs real application binaries. It > is the one that they are verifying certain properties about. Think of > the Haskell version as providing a low-level formal model. > > Separately, they are doing an implementation in a constrained subset of > C (I think it is C rather than C++, but I'm not sure). The idea is to be > able to translate this implementation into their theorem prover as well, > and then to show that it corresponds to the Haskell low-level model. So > there *is* an implementation in C. > > There are many missing links in their verification story, but it is very > promising, and it is much further along than anyone else has managed to > get. > > Unfortunately, I suspect that the C implementation will never be > released in open form. The seL4 team has formed a company, and most of > the work is being done by that company. They have 30 people employed > already. For those of you who don't have any experience with corporate > finances, 30 people cost between $6M US and $7.5M US per year. Perhaps > 15% less in Australia, but that isn't important to the point I am > making. The company has been operating for at least two years. If you > are externally funded (as they are) the expected return on investment is > generally around 35% per year, compounded annually. In effect, they have > taken out two loans of ~$7.5M each (one for each year). To pay that loan > off, the company would require a valuation *today* of $23.78M. If they > have to wait another year to be saleable, they will need $42.22M. > > You can see that the slope is very very steep. Even if they *want* to > release everything, the investors probably will not allow them to do so. > > This, by the way, is why The EROS Group chose *not* to fund our > development using investor dollars. > > Jonathan _______________________________________________ L4-hurd mailing list [email protected] http://lists.gnu.org/mailman/listinfo/l4-hurd
