>> в ЯП фишки, позволяющие делать проверки в компайлтайме.
> Я конечно понимаю что CS у россиян не в почете, но до
> того как умничать - наверное азы типа halting problem стоит почитать?
> Полный анализ поведения программы выполнить невозможно. Тюринг предствил математическое
> доказательство, взяв для примера довольно простой случай, изучающий завершится ли программа Существует такая вещь, как SMT-solver'ы. Они могут проверить граничные условия, заданные для какой-то функции и её частей.
Язык Ada Spark https://en.wikipedia.org/wiki/SPARK_(programming_language) такое может
и пример проекта http://blog.adacore.com/tetris-in-spark-on-arm-cortex-m4
Для языка Си давно уже существует Frama-C https://en.wikipedia.org/wiki/Frama-C который точно так же позволяет гарантировать некие условия, выполняющиеся функцией.
Эти вещи не применяются в разработке массового ПО, в том числе опенсорцного потому, что господа сишные хакеры в большинстве своём малограмотны в CS и не "заточены" под долгую кропотливую работу, дающую корректный результат. Также, Frama-C предполагает, что в некоторых случаях разработчик будет пользоваться Coq, а это уже очень требует очень высокий уровня владения довольно специфичной математикой.
Военного происхождения Ada Spark - простой, как кирпич и ничего такого не требует, хотя он и менее мощен, чем научная французская Frama-C, зато язык Ada гораздо более стандартизирован, чем Си, и от него не стоит ждать неожиданностей. Но с ним другая беда - во-первых, он не си, а паскаль, там видите ли begin и end, от вида которых у байтогрызиков начинается фрустрация. Во-вторых, в бесплатном виде он распространяется только под GPL, а большая часть проектов имеет двойное лицензирование - если они хоть кому-то будут продаваться за деньги. Коммерческий же Spark стоит дорого, примерно как четыре колеса от джипа, но у байтогрызов зачастую нет не то, что джипа, а даже и тоёты, они на велосипедах ездят, с зеркалками, интересные проекты делают. Денег у них нет.
Поэтому пользователи OSS так и будут ловить CVE, к ним будет лезть NSA и все прочие кибержулики. Потому что во главу ими была поставлена хакерская скорость разработки, а не промышленная надежность. Пришёл упорный инженегр Линус, быренько наrовнякал реализацию Posix, раньше Столлман доделал своё, и теперь нам всем с этим жить, мода задана на много лет вперёд. 12309! Я думаю, что финскому жирному пингвину помогли придти к успеху те самые люди, про которых Сноуден рассказывал. Чем больше дыр и ненадёжного софта - тем лучше для этих. Люди работают, понимать надо.
Более того, поскольку программистская культура в общем-то едина, те же самые скоростные багоделы пишут и коммерческий софт. Это модно.
PS: доказанное ядро на Ada Spark, https://muen.sk/
Понимаете ли, на паскале с пред- и пост- условиями написали ядро, без дырок.
PPS: по бенчмаркам на https://benchmarksgame.alioth.debian.org/u64q/ada.html Ada работает примерно со скоростью Си и иногда обгоняет С++, причём Ada у них старая, 2005, а не 2012
