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

[anon@att.net]

seL4 is just another  subset of the L4 project, which has nothing to 
do with Ada or an AdaOS.  Now, there are a number of Ada OS projects
which core code are based on the L4 project, like MaRTE (last update 
uses GNAT 2009), RTERMS (2008), and OpenRavencar (based on GNAT 3.13).

For Ada purest, to do a AdaOS, like the one I an working on, the entire 
code must be written in Ada with exceptions for macros for assembly code 
(using the Ada Machine_Code package) that extents Ada API to allow 
hardware instructions, such as the CPU's I/O instructions. And some of 
these macros instructions include code used to switch the processor from 
initial 8/16 bit 8086 state (power up/reset) to a 32-bit protected mode 
and then detects and if possible switch to 64-bit mode during the boot 
phase.

The AdaOS should be able to handle both 32-bit/64-bit code and maybe a 
some trusted special case protected VM code. As for languages, the 
OS should have Ada as the primary languages. If a secondary language is 
desired then it's compiler must be written in Ada. This means that 
others projects like openGL should be written in Ada instead of just 
porting the project code to the new AdaOS after a C compiler is 
written in Ada and then binding the code to the AdaOS.

The AdaOS, also should be a stand alone system that can work 
within a virtualization environments with some small limitations 
caused by the VM engine unless the VM is also, written in Ada and 
the AdaOS is the host OS.

Then there's the compiler while GNAT is an OK compiler it will not 
work for the new OS, we need a compiler from the ground up written in 
Ada that can produce code for a number of OS including an AdaOS that 
does not depends on any host OS or a design implementation like GNU 
which is based on C/C++. That way the new Ada compiler could be 
easily ported to the new OS without any other language or groups 
involvement.

But just having an AdaOS will not increase the usage of Ada. This 
might change if and only if the AdaOS was a complete and robust OS 
that could go against Microsoft Windows and Apple's OS X. But 
most people writing an AdaOS normally stop after they finish the 
initial kernel. Which mean an AdaOS will never become robust enough 
to even equal any OS used today. much less compete with those 
OS. 



In <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com>, kug1977@web.de writes:
>Hi,=20
>
>NICTA and General Dynamics C4 Systems have made seL4 Open Source (GPLv2/ BS=
>D). seL4 is the world's first operating-system kernel with an end-to-end pr=
>oof of implementation correctness and security enforcement and claims to be=
> the world's most highly-assured OS.
>
>As seL4 is written in C and some ASM and the proofing was done with Haskell=
>, I asked myself: Can we use this kernel as a base to develop a real AdaOS =
>with Spark to proof it's correctness? seL4 is a real microkernel, so it's n=
>ot like porting Linux or Mach to Ada.=20
>
>L4 has Real-Time capabilities, a capability based security system, Task and=
> Threads, high speed IPC, so it might fit everything from embedded to serve=
>r. With Genode (http://genode.org/) there's a test environment with differe=
>nt kernels (incl. L4) and a tool chain, so we must not start from scratch.=
>=20
>
>Doing an OS in Ada / Spark, might attract some people to use Ada instead of=
> C. And having an OS written in Ada, seems not only my dream. :-)
>
>-kug1977