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

[gvdschoot@gmail.com]

On Wednesday, July 30, 2014 7:58:33 PM UTC+2, an...@att.net wrote:
> 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. 
> 

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? Let's just forget the desktop or tablet. These areas are untouchable unless you are very lucky.

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