From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.66.124.199 with SMTP id mk7mr1641093pab.15.1406881674311; Fri, 01 Aug 2014 01:27:54 -0700 (PDT) X-Received: by 10.140.19.213 with SMTP id 79mr55432qgh.5.1406881674256; Fri, 01 Aug 2014 01:27:54 -0700 (PDT) Path: border2.nntp.dca1.giganews.com!nntp.giganews.com!h18no11836333igc.0!news-out.google.com!b3ni5177qac.1!nntp.google.com!j15no3745840qaq.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 1 Aug 2014 01:27:54 -0700 (PDT) In-Reply-To: <67392172-e7c5-473b-ab8b-f9f56ed0d71f@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=92.109.179.4; posting-account=uePmQwoAAADTqdMkQ5mqQNa8zVpjxCa1 NNTP-Posting-Host: 92.109.179.4 References: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com> <9509bda5-4429-4e2c-ac97-bc7959257006@googlegroups.com> <67392172-e7c5-473b-ab8b-f9f56ed0d71f@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <485a93a1-8920-4139-8563-591dba79d68d@googlegroups.com> Subject: Re: seL4 as base of an AdaOS with some Spark proofing? From: gvdschoot@gmail.com Injection-Date: Fri, 01 Aug 2014 08:27:54 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Xref: number.nntp.dca.giganews.com comp.lang.ada:188068 Date: 2014-08-01T01:27:54-07:00 List-Id: 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?=20 >=20 > 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. To= day it's the most used OS in Servers and embedded products. And it's not an= microkernel, so more code then L4.=20 >=20 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 sam= e 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 talki= ng 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 critic= al part should moved over to Ada sooner than later, but it's a better situa= tion 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 l= ot of design decision are done and we can learn from the mistakes they've d= one. Nobody has to start from "primordial soup" of OS design, it more a cha= nge of the implementation language. For the kernel yes. But if you want a complete OS, there are a lot of thing= s more. GUI for instance is a can of worms. To POSIX or not to POSIX? Alien= ate because of security or accept a wide range of attack surfaces? > > Here is another idea. Let's for instance instead focus on tools that ca= n automatically translate C source code to Ada. >=20 > What I know about C, you won't and I'm very sure you can't translate it t= o Ada in an automatic way. But you can use the seL4 code base and migrate i= t to Ada and use the Haskell Code to see, where the "big money" put the eff= ort 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 shri= nk.=20 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 th= is 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 doi= ng right now is talking.