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