-------- Original Message --------

> OK, let's do it. Let's start with a PID1 that does nothing but run a
> single shellscript and receive incoming signals. The 16 line C program
> for a PID1 that runs a shellscript shellscript and nothing else can be
> seen toward the bottom of http://ewontfix.com/14/ . The Suckless Tools
> version, which is more like 83 lines plus some .h code and responds to
> incoming signals, can be quickly and simply downloaded with:
>
> git clone git://git.suckless.org/sinit
>
> Serious business, tell me how to write the 16 line
> only-runs-shellscript version in Ada Spark.

I think something like this Spawn crate will be in Ada not Ada SPARK and not
provable to Silver level easily.

https://github.com/AdaCore/spawn

The trick would be to make very simple interfaces to any C or syscalls or
running system or fork and exec etc. so that the inputs and outputs to the Ada
SPARK could be proven more easily not to be able to crash the core Ada system.
Keeping it simple as Rainer (and myself actually) loves to do is in essence the
easiest way to make proving it is absent of runtime errors easier. Obviously any
C code is not provable to never crash atleast not with gnat prove. If the core
is extremely simple then perhaps it is pointless but I expect any fully fledged
init (runit is 24k) isn't obviously crash free.

I would love to help but today is not that day, sorry.

-- 
All the best,
             Kevin Chadwick