Le 08/04/2026 à 14:50, Kevin Chadwick via Dng a écrit :
>
> -------- 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.
>
    The Ada program, needing to interface to the C library, the
wrappers for the C functions would need to use the package
Ada.Unchecked_Conversions, which certainly does not pass SPARK controls.
So that there remains essentially nothing for SPARK.

    Since the essence of this program (if it is small) is only to
invoke system-calls, there does not seem to be any point in writing it
in another language than C. Writing it in shell is interesting, but only
demonstrative.

--     Didier