Язык C, как прослойку, часто используют для того, что бы поддержать бОльший спектр аппаратных платформ.

Новый то он новый, конечно. Но в отличи и от старых языков, приложение на таком новом может быть формально верифицировано. В частности Р - язык взаимодействующих автоматов, корректность которых можно формально доказать. А SPIN, например, позволяет формально доказывать наличие гонок в коде.

Я не предлагаю использовать Р или SPIN. Но пример и путь микроядра seL4 (https://sel4.systems) мне кажется правильным. Разработчики seL4 пошли по пути разработки собственных инструментов по генерации и верификации С-кода (сами инструменты сделаны на Haskell). Практическое программирование должно больше опираться на формальные математические методы, которые хорошо проработаны в научном программировании.

Хотя текущее направление работ в Rust (например https://kha.github.io/2016/07/22/formally-verifying-rusts-bi... и http://ticki.github.io/blog/a-hoare-logic-for-rust/) мне нравится.

Еще раз, Эрик говорит про устаревшие практики программирования. Я с этим согласен полностью и отметил лишь тот момент, что просто смена языка программирования может не дать результатов если не подкрепить их теорией.
А теория должна быть заложена в новый язык. Компилятор этого нового язык может быть как самодостаточным (с свои рантаймом (например MLton)) так и являться утилитой, которая создает С-код не требующий рантайма больше чем стандартная библиотека С. Самодостаточный вариант не всегда возможен, т.к. в общем случае существуют аппаратные ограничения.
И хотя в текущем случае с NTPsec аппаратные ограничения на память можно считать отсутствующими. Ограничения на использование CPU существуют (многопоточность и гонки никуда не денутся (как в приложении так и в рантайме языка) и хочется их поймать до этапа эксплуатации)