On 4/4/2026 00:35, Didier Kryn wrote:
> Le 03/04/2026 à 11:23, Kevin Chadwick via Dng a écrit :
>>
>> -------- 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).
>>
>     Ada is really made for large or complex applications. OTOH, I don't
> think pid 1 should be complex. There are versions of init written in C
> which are so tiny that almost everybody with a basic knowledge of the
> language can review, and of course the most brilliant programmers do.
> This makes a lot of reviewers. This is the main problem with systemd:
> the size and the complexity; of course it is worsened because it is
> written in C, and , why not C++.
>
> --     Didier

Indeed, there are tiny init systems designed for containers that are
less than 1000 lines of code:

https://github.com/krallin/tini - 688 LOC

https://github.com/Yelp/dumb-init - 340 LOC

You can go even further still with this minimal example by Rich Felker,
the musl libc developer:

https://ewontfix.com/14/ - 22 LOC

Or his improved version:

https://github.com/richfelker/minimal-init - 50 LOC


--
Tom