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.68.209.130 with SMTP id mm2mr1540752pbc.3.1406878924119; Fri, 01 Aug 2014 00:42:04 -0700 (PDT) X-Received: by 10.140.23.163 with SMTP id 32mr10378qgp.8.1406878924063; Fri, 01 Aug 2014 00:42:04 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.glorb.com!h18no11815294igc.0!news-out.google.com!b3ni5434qac.1!nntp.google.com!v10no3671021qac.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 1 Aug 2014 00:42:03 -0700 (PDT) In-Reply-To: <9509bda5-4429-4e2c-ac97-bc7959257006@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=62.245.202.100; posting-account=3ciIaAoAAAA6pCfildcdAcuc3UQuirtL NNTP-Posting-Host: 62.245.202.100 References: <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com> <9509bda5-4429-4e2c-ac97-bc7959257006@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <67392172-e7c5-473b-ab8b-f9f56ed0d71f@googlegroups.com> Subject: Re: seL4 as base of an AdaOS with some Spark proofing? From: kug1977@web.de Injection-Date: Fri, 01 Aug 2014 07:42:04 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:21370 Date: 2014-08-01T00:42:03-07:00 List-Id: > So you want to compete with the big guys? You want to compete with the mu= lti billion dollar companies? With what? Ideas? Do you know how many man ye= ars it takes?=20 Well, I remember a time an unknown student posted something about a unix ke= rnel and a big fellow in theoretical OS design called the idea stupid. Toda= y it's the most used OS in Servers and embedded products. And it's not an m= icrokernel, so more code then L4.=20 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 situati= on 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 don= e. Nobody has to start from "primordial soup" of OS design, it more a chang= e 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 effor= t in to check correctness. And as written before, a lot of checks we can fo= rgett, because they are part of Ada already. So the code base should shrink= .=20 -kug1977