The Kernels for all major operating systems are written in C; C is also used for the majority of embedded devices which perform the small miracles around you. C is everywhere.
Yes, but those kernels aren't developed according to any functional safety standards, so they're the typical jumble of vulnerabilities.
It depends if that's the case for the embedded devices.
There are also software verification tools that use binaries instead. That's how seL4 gets verified. This way you're safe from compiler bugs.
Well, C actually does have very good verification tools, so if they are used it could be a reasonable choice.
The problem is that commercial SW development is incompatible with the use of such tools or the associated safety-critical processes. The extra time, process, competences would make a company much slower than the typical bullshit move fast and break things start-up.
C is already the undisputed king of running everything and on everything, no one who writes C needs to seek validation like this.
> The certification and correctness part is made easier by using software verification tools. One such tool is Astrée. It is a static code analyzer that checks for runtime errors and concurrency related bugs in C projects. This also leads us to the answer for why a lot of mission-critical code is written in C. Its because there are a lot of static analyzers and software verification tools for C.