Apparently SEL4 and predecessor sel3 has been around in various forms since its inception back in 1988.

I recognised it because back in 2009 I saw an article about the worlds first fully proofed computer code, of 40 kilobytes in size. the aricle stated that similar treatment could be given to device drivers, which were smaller. My first thought was, it says Microsoft is paying for this, it has to be a microkernal of some sort.

Apparently it is now used in Apple products, having options for x86, x64, Mips, ARM, Linux etc

What is the main difference, given Sel4 has memory protection, and Exec doesnt, in that 40k of code, given everything else mentioned about semaphores, message passing, preemptive multitasking, introduced in 1998? looks extremely similar to Exec, presumably because when working with highly optimised assembler at the start, theres very few different ways of doing things?

https://en.wikipedia.org/wiki/L4_microkernel_family

Available in GIT hub Open Source since last year. But its not all in a nice single archive that I can see. Then again, due to net abuse by companies, I run a lot of blockers.

Theoretically we can do formal methods on AOS by using BrainF**k intermediate code, which was created on Amiga, bu that a big change, and coders dont seem to like the computer doing all the work. Hey look, you have a buffer overflow here, etc.

Is there any translation, emulation, comparison between SEL4 and Exec, that would permit the creation of Exec in such a manner, or AOS on such a kernal, or does the conflict between Proprietry and Open Source, Commercial and GPL, or just programmers and creators create an uncrossable chasm that can never be bridged?

After all, the code might be secure, but its still being run on gate perfect rigid form silicon logic that has no error correction, sacrificial logic, honeypot etc. That is, why cant we build a 300% larger proofed CPU into a FPGA, designed with reliability in mind, given error correction systems start at 10% extra logic? I mean, having a proofed kernal running on a fixed hardware is all well and good, but when was the last time you had hardware reliably remain in the same state?

_________________
The older and more respected a scientist is, the longer it takes to prove him wrong.