-------- 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).
--
All the best,
Kevin Chadwick