> Далеко не все ограничения MISRA C могут быть проверены автоматически, Более того, согласно Тюрингу нельзя даже определить - повиснет программа или нет. Есть интересные способы прострела пяток. Например, можно обслуживать аппаратный вачдог в прерывании таймера. Заметь, я ничего не сказал про ЯП. Так тупануть можно на любом ЯП позволяющем системное прогрмамирование МК.
> главное другое - MISRA, фактически, предоставляет другой язык,
Язык тот же самый - Си. С джентльменскими договоренностями про dos и donts нацеленными на уменьшение классов ошибок. Писать без ошибок можно и на полной версии, DJB проверял. Так навскидку. Возьмем tweetnacl. Достаточно маленький чтобы прочитать и достаточно большой чтобы делать что-то полезное человечеству. Вот где он может облажаться? Память не выделяет, опасных операций не делает, внешних зависимостей одна штука - получение извне рандома. А вот какие-то там хипстерские рантаймы делающие непонятно что - всегда подкинут свинью. Сколько человек на планете вообще разбирается - будет ли вон та операция в rust константой по времени, например? А для криптографии это важно - зарубает целый класс атак, делающих выводы по разному времени выполнения. Такие вещи могут быть абсолютно фатальны. Скажем достаточно необдуманно сравнивать пароль чем-то типа memcmp и далее можно просто глядя на дельту по времени угадывать его по отдельным буквам. И сложность подбора пароля из 10 символом станет не 256^10 а 256 * 10, что как-то совсем не айс. На сях подобные вещи делать сравнительно просто, потому что язык достаточно простой и рантайм опционален и не пытается втиснуться вообще везде, типа чистой математики.
> с Си. Также, это свидетельствует о признании проблемы со стороны промышленности.
Разработка софта вообще очень проблемная отрасль. У прогрмамистов есть такой анекдот: если программа с первого раза заработала правильна - вырубай скорее и ищи ошибку.
> - Выпустить нечто мало пригодное для надёжного прогаммирования.
Guns don't kill people. Языки прогрмамирования не делают ошибок, ошибки делают люди. Ты чего хочешь? Заменить дорогих элитных сишников, понимающих что они делают на хипстерских обезьянок дешевле? Чудес не бывает, обезьянки не будут понимать как это работает, сложный рантайм все усугубит. Тех кто будет реально понимать что, как и почему работает будут считанные единицы на планету, будет множество неочевидных failure modes. Результат не заставит себя ждать. Посмотри вокруг. В этих php, python, ruby и прочих вообще нет работы с указателями. Но это не мешает хакерам взламывать большинство серверов через дырявую вебню. А просто потому что вебмартышки уверены что за них рантайм подумает. Иногда это так, но Боби Тэйблс и его друзья готовы с этим тезисом поспорить. Достаточно успешно, кста.
> - Начать применять его для критичных к корректности задач.
Люди применяют для задач инструменты которые работают. Си используется в критичных задачах десятилетиями и работает это получше других инструментов. Системное программирование вообще к надежности требвательно выше среднего. В ядре системы одна ошибка - и ты идешь перезагружать систему. Хороший стимул не лажать в коде.
> - Получить кучу проблем, и объявить половину возможностей небезопасными.
Системное програмирование подразумевает возможность прострелить себе пятку. Разумеется это не безопасно. Жить вообще вредно - от этого умирают.
> - Выпустить об этом документ и начать продавать его за деньги.
> - Выпустить утилиту для проверки на соответствие документу и начать продавать его за деньги
Требования достаточно общеизвестны, утилит более одной. На том же ядре Linux например гоняют с дюжину разных анализаторов периодически. И живые люди код читают. Но все-равно иногда пролезают ошибки. Кода много, не все взаимодействия между разными частями - тривиальные. И никакой ЯП не спасет тебя от этого сам по себе.
> - Всё равно иметь кучу проблем, но продолжать использовать.
А еще можно верить в серебряные пули, нанимать долбоклюев ничего не смыслящих в безопасности и при этом в силу глупости надеяться что врожденный кретинизм програмера лечится заменой ЯП, а не заменой програмера. Только как там в басне говорится: вы друзья, как ни садитесь...
