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

[gvdschoot@gmail.com]

On Friday, August 1, 2014 9:42:03 AM UTC+2, kug...@web.de wrote:
> > 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. 
> 

I also said: "These areas are untouchable unless you are very lucky."
The problem with Linus Torvalds is that he doesn't scale very well. The same with RMS.

> 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.

I like that idea.

> 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 am not sure having a microkernel makes the overall code size smaller. You still need drivers, filesystems etc.. They only don't run in the critical path.

Another benefit of microkernels is that it doesn't matter in what language a server is written in. A mixed C / Ada / lang-x is perfectly fine.

What I would like to say is that having a running system is very important. From there on things can gradually improve.

> 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.

For the kernel yes. But if you want a complete OS, there are a lot of things more. GUI for instance is a can of worms. To POSIX or not to POSIX? Alienate because of security or accept a wide range of attack surfaces?

> > 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. 

Just because it hasn't been done before doesn't mean it is impossible. For instance the Go (golang) team in the person of Russ Cox is working on c2go and the approach he takes is unconventional. There is presentation about this on youtube.

However if C and Ada can coexist there is no need for it to get a system up and running.

The major problem that I see is the organization. The only thing we are doing right now is talking.