Re: seL4 as base of an AdaOS with some Spark proofing?

[kug1977@web.de]

> So you want to compete with the big guys? You want to compete with the multi billion dollar companies? With what? Ideas? Do you know how many man years it takes? 

Well, I remember a time an unknown student posted something about a unix kernel and a big fellow in theoretical OS design called the idea stupid. Today it's the most used OS in Servers and embedded products. And it's not an microkernel, so more code then L4. 

The idea was, that if we show, that you can do a whole microkernel in Ada (and some part on top of it are written in Ada/ Spark, i.e. ironsides (DNS), AWS (WebServer), we can show, how to make a secure OS everybody is talking about, but nobody can deliver at the moment.

And having L4 microkernel make the source code smaller. At the beginning we have to use parts of other OSes, we have to integrate C code  and critical part should moved over to Ada sooner than later, but it's a better situation than Linux and BSD were in in the 1990er.

I know, that a lot of work has to be done. But L4 is a proven design. A lot of design decision are done and we can learn from the mistakes they've done. Nobody has to start from "primordial soup" of OS design, it more a change of the implementation language.

> Here is another idea. Let's for instance instead focus on tools that can automatically translate C source code to Ada.

What I know about C, you won't and I'm very sure you can't translate it to Ada in an automatic way. But you can use the seL4 code base and migrate it to Ada and use the Haskell Code to see, where the "big money" put the effort in to check correctness. And as written before, a lot of checks we can forgett, because they are part of Ada already. So the code base should shrink. 

-kug1977