> А я вот то ли у Э. Дейкстра, то ли у Хоара читал, что тестирование
> не показатель отсутствия ошибок.

Для себя я предпочитаю верить своим глазам и думать своим мозгом. И я вижу что в случае крупного кода - более-менее адекватны только сложные комплексные мероприятия и вон то это их часть.

При том тесты бывают разные. Скажем юниттесты проверяют что накодили блок кода именно так как было задумано. А более глобальные - что оно после интеграции в целое ведет себя адекватно, т.к. на стыке взаимодействий кусков тоже можно отхватить чудес. А бывает вообще fuzzing. Потому что в даташите может и написано что датчик может выдавать от сих до сих, но, знаете, реальный мир может иметь свое мнение на этот счет и сдруевший датчик влет накормит систему какими-то совершенно неадекватными значениями. Если при этом софт навернется - ну, блин, ой. Поэтому долбежка рандомом не панацея но - при достаточной интенсивности успешно ловит неведому хрень.

> Т.е. ошиблись классики ?

Скорее имели синтетическое представление не от мира сего - особенно его актуальной версии. Могу сказать что всякие математические верификации имеют большую проблему: не работают для более-менее крупного софта из-за комбинаторного взрыва, при котором доказать что-то для ВСЕЙ системы в СБОРЕ что-то становится малореально. А даже если вы проверили отдельные мизерные кусочки это не доказывает что они вместе делают что-то адекватное. Более того - в штуке размером с самолет чертова куча разных систем взаимодействующих между собой. Писаных разными кодерами. И то что 2 разные тимы одинаково поняли формальное описание и все краевые случаи - мягко говоря не факт.

Как угодно но мир стал сложнее. В нем стало больше данных и все хотят больше фич. Если первые авиаторы сидели на воздухе, дергали рычаги от и до сами, то теперь хотят систему автоматической посадки, спутниковую навигацию, анализ топологии местности - и предупреждение что впереди гора, приборов постепенно стало столько что пилоты начали зашиваться, особенно в ситуации отличной от идеала. Не говоря о том что в сотнях проводков, тросиков и чего там еще все время что-то барахлит и из-за отсутствия средств самодиагностики хрен поймешь что. А разбирать самолет от и до перед каждым вылетом никто не будет. И пилот сталкивается с дилеммой, лететь ему абы как или резко и дорого обломать всем кайф под угрозой линча руководством - и все же пусть техники более плотно займутся. Заодно оказалось что умные машины могут лучше знать параметры машины и например не дать пилоту делать явно провальные действия. И ясен фиг логика всего этого - ни в раз не тривиальная. Как и коммуникации с продвинутыми датчиками, перекидывания кучей сообщений по шинам с пачкой систем и проч. Топологически современный транспорт это ездящие, летающие и плавающие сети компьютеров и микроконтроллеров. Это совсем другой паттерн. Со своими специфичными проблемами - но это лучше чем то что было до этого, назад никто не вернется.

> с полсотни докторов наук Гриса переводили.

Я давно не оперирую переводными материалами, в том числе и потому что насколько переводчики в курсе тематики и не наломают дров, угрохав изначальный смысл - отдельный вопрос.

> Причём вышло лучше, чем в оригинале на Globish)

Да вот как бы вам сказать... азы antibug coding годные для практических применений в управляющих системах мне вот например в основном в libera.chat програмеры объяснили + несколько ресурсов жестких профессиональных эмбедеров, которые гамна лаптем покушали на практике. То что так кто-то в РФ может я честно говоря сильно сомневаюсь. А вон та магия нехило работает, я более-менее смог в направление и в принципе я начинаю немного доверять своим сишным фирмварям. Бывает так что даже с 1 раза работает как надо, сразу без багов.

А некое "практическое" понимание топика - парочка firmware safety guideline'ов от компаний типа STMicro которые расписывают с чем вообще можно столкнуться (не, теоретики про половину этого тупо не в курсе и в их рассуждизмы сие зачастую не включено, так что система будет себя вести не так как предсказано ими). Это больше для автомотивщиков, но там видите ли люди тоже мрут если ECU или ABS сделает что-то не то, а это кучка проциков с фирмварой да исполниловкой и сетью - по сути "fly by wire lite". Стандартный паттерн дизайна систем.

Авиаторы еще более замороченные, у них всяких рулесов и гайдов еще больше. На что были причины. Тем не менее что касается софта и сертификации, как показали некоторые примеры это все не очень эффективно работает, если боинг игнорит вопли пилотов и даже падение 1 самолета от дурного алгоритма MCAS, и требуется чтобы еще 1 боинг расплющило точно так же, так что тогда даже какой-нибудь посторонний NTSB понимает что тут где-то подстава и имеет всех по полной.