Kevin Chadwick via Dng <dng@???> writes:
> -------- 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).

Somehow, this reminds me of answering "This wouldn't have happened in
Mandarin!" when someone points out an error in an English text ...