Kevin Chadwick via Dng said on Fri, 3 Apr 2026 10:23:31 +0100

>-------- Original Message --------
>
>> which uses assert for invarant checks in the context of the init
>> process. Should these asserts ever trigger, they'll stop the program
>> via abort which will cause a kernel panic because init is special
>> can just exit in case of a runtime error. But why would people
>> programming in the context of init take that into account?
>
>Ada SPARK would be a great choice of language for pid 1 actually. As
>you could I guess quite easily prove it to Silver level and be sure it
>could never crash (AORE; absence of runtime errors).

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.

Thanks,

SteveT

Steve Litt

http://444domains.com