В гости к
fun evenSqares {n:nat | n % 2 == 0 && n >= 4 %% n != 10}(x : int n) : int(n*n) = x*x
Выяснилось, что народ не знает различия между верификацией и валидацией.
Я их вечно путаю, так что объясняю просто: Та, которая «ве», - она про «Кто виноват?», а которая «ва», она про «Что делать?» (Кто не застал уроков литературы советских времён, пусть придумает что-то посовременнее.)
Верификация нужна для того, чтобы программисты не наделали ошибок, не выдумывали «более лучшие решения, потому что знаем мы этих идиотов, не понимающих великого PHP», а запрограммировали то, что приказано. Верификация работает с моделями и проверяет, чтобы они были воплощены правильно.
Она может быть сложной, но существует множество методов, в основном административных, позволяющих снизить вероятность ошибок, как отсекая процессы, ошибки создающие, так и вылавливая ошибки просочившиеся.
Качество верификации определяется метриками надёжности типа наработки на отказ. И стоимость растёт экспоненциально при приписывании сзади очередного нуля.
Сервер на сто тысяч параллельных соединений, которому разрешено каждые пять минут пару-другую потерять, и сервер обслуживающий тысячу стрелок и пять поездов, которому не позволено выдавать ерунду чаще, чем раз в тысячу лет - это проекты совершенно разных ценовых категорий.
Mission critical - это то, где за ошибку можно получить не только штраф, но и конкретный уголовный срок. Особенно, если ошибки стоят не только кучу денег, но ещё и человеческие жизни.
Ни один инженер не подпишет протокол, если знает, что в системе явные баги. Ни один менеджер не хочет сесть, если выяснится, что на протоколе не было подписи. Потому не надо удивляться, что в этой области развели бюрократию.
При этом всё равно идут изменения в спецификацию по мере нахождения ошибок (в том числе, после тестирования) или получения новых указаний. И каждое изменение проходит полный цикл проверок. По этой причине любимые теоретиками и веб-разработчиками методы, советующие сначала делать, а потом думать, в таких проектах не проходят.
(Конечно, бывает всякое. Видел я и как углы срезают самым безобразным образом. Но это не от большого ума.)
Теперь вернёмся ко второму слову.
Валидация - это не столько про само программирование, сколько про техническое задание. И для неё нет общих методик. Область эта очень болотистая, требующая хорошей соображалки, аналитических способностей и большого опыта.
Потому что это то, где наши модели сталкиваются с реальным миром.
Сложнее всего валидировать что-то космическое. По крайней мере из того, что я видел. Единственная область, где я после двух месяцев работы ещё нифига не понимал. (Впрочем, книжек про это дело практически нет, приходилось информацию выуживать из достаточно хаотичных текстов.)
Колебания топлива в нетривиальных условиях в нетривиальном сосуде, граничные параметры эмуляции которого заданы таблицей производителя с кучей дырок. Вращательное движение неравномерных несимметричных объектов. Торможение атмосферой. Закручивание магнитным полем Земли. Притяжение Луны. Не соответствующая параметрам изготовителя точность звёздных датчиков...
Всё это складывается в дикую систему. Одна матрица учитываемых параметров занимает на распечатке стол целиком.
И всё это должно работать в реалтайме. Причём, в любое время может прилететь какая-нибудь вредная частица и выбить в памяти пару битов.
Математика алгоритмов управления положением и динамикой там безумная. Причём, на неё со всех сторон накладываются очень жёсткие ограничения как по производительности бортового компьютера, так и по точности измерений или действий управляющих элементов.
И рабоатют там крутые люди. Которые могут и ФП, и ООП, но предпочитают писать на голом C, чтобы быть уверенными в том, что софт делает на самом деле то, что должен.
В другой стороны, есть в спутниках и софт управления в смысле включить-выключить. Он простой и не интересный. Но требует всех плясок с бубнами, потому что должен быть надёжным. А это ужасно скучно. Оттого в эту область особые таланты не идут. Все гении давно сбежали туда, где повеселее и похалявнее.
Таким не то, чтобы строчку сверху показывать нельзя. Им от слова «монада» страшно станет.
Так, для примера: когда в одном проекте (не космос, а попроще, но mission critical) я предложил для одного эмулятора многопоточное решение (достаточно банальное), понять, о чём я вообще говорю, мог только один человек. Причём, это был совсем не Главный Аналитик. Который вообще такими вещами не интересовался. «Потому что операционная система реалтайм обеспечивает, значит ничего неприятного произойти не может.»
А надёжность при ошибках памяти рассчитывал студент в качестве курсовой. У него сначала получилась наработка на отказ, от которой начальник схватился за голову. Но потом он проверил, пересчитал и исправился.
Насколько знаю, на первом же полевом испытании полученная система отказалась реагировать на внешние раздражители и впала в нирвану. Что, собственно, соответствовало критерию надёжности, определённому менеджментом как отсутствие выдачи команд ошибочных.
Ну так вот, «тупые методы», «тупая бюрократия», «тупые процессы» и «тупые языки программирования», собранные вместе, позволяют людям, не хватающим звёзд с неба, производить такой софт, что космические аппараты не заваливают миссии, ракеты не взрываются, самолёты не падают, поезда с рельс не сходят и машины не разгоняются, когда надо тормозить.
Впрочем, Тойота, подарившая вебовским кудесникам волшебные слова типа «lean» и «kanban», наглядно показала, что бывает, если экономить на «устаревших методологиях».
no subject
Date: 2016-02-11 03:22 am (UTC)no subject
Date: 2016-02-11 04:17 am (UTC)fun evenSquares {n:nat | n % 2 == 0 && n >= 4 && n != 10}(x : int n) : int(n*n) = x*x>...позволяют людям, не хватающим звёзд с неба, производить такой софт, что космические аппараты не заваливают миссии, ракеты не взрываются, самолёты не падают, поезда с рельс не сходят и машины не разгоняются, когда надо тормозить.
Тут стоило добавить "обычно". А то ведь регулярно и заваливают, и взрываются (каждая десятая или около того), и бороздят просторы мирового океана.
no subject
Date: 2016-02-11 05:39 am (UTC)Может заплатить за неудачи все же дешевле-выгоднее, чем нанимать "хватающим звёзд с неба" и долго верифицировать? А людей новых нарожают, тем более что от долгой верификации люди тоже могут умереть, не дождавшись вертолета или светофора.
no subject
Date: 2016-02-11 06:31 am (UTC)А ракеты заваливаются в основном не из-за программистов, а из-за того, что им техзадание неполное дали. В том числе и со знаменитым Арианом.
no subject
Date: 2016-02-11 06:35 am (UTC)no subject
Date: 2016-02-11 07:38 am (UTC)no subject
Date: 2016-02-11 07:56 am (UTC)Мода на такое - потому что веб! Ну упало, ну хрен с ним.
А стоит хоть краешком прикоснутся с реальным миром, хоть одним датчиком - и все приехали: лезут погрешности, датчик может подвирать, зависимости мало что нелинейные да еще и дырками.
no subject
Date: 2016-02-11 08:11 am (UTC)no subject
Date: 2016-02-11 10:26 am (UTC)Какая мода? Тот язык знают полтора человека.
Какой веб? Ни я, ни пользователи того языка вебом не занимаются. В вебе такое не применяется.
Какой упало? Такие программы как раз не падают (при работающей аппаратуре, конечно).
В условиях реального мира и датчиков агитируете за говно и палки вместо математики?
no subject
Date: 2016-02-11 10:32 am (UTC)no subject
Date: 2016-02-11 10:48 am (UTC)no subject
Date: 2016-02-11 11:02 am (UTC)Во многих случаях "теоретическое" решение слишком сложно. Особенно, если в системе слишком много связей. Например, есть случаи, когда правильно использовать таблицы вместо формул.
no subject
Date: 2016-02-11 11:17 am (UTC)no subject
Date: 2016-02-11 01:28 pm (UTC)no subject
Date: 2016-02-11 01:40 pm (UTC)no subject
Date: 2016-02-11 03:44 pm (UTC)no subject
Date: 2016-02-11 05:00 pm (UTC)Э?!
Инженеры знают
Это, вообще говоря, прямая обязанность инженера - в его области знаний и умений ЗНАТЬ И ПОНИМАТЬ несовершенства мира сего...
no subject
Date: 2016-02-11 05:25 pm (UTC)no subject
Date: 2016-02-11 09:09 pm (UTC)Причина, по которой там оказываются такие люди, как-то не описана. Но как-то раз в этом блоге встречалось нечто вроде "стали заниматься серьёзными(!) делами, а не сбежали за деньгами в стартапы". Серьёзными, Карл!
no subject
Date: 2016-02-11 09:35 pm (UTC)Тут такое дело...
Есть люди, которые впадают в экстаз от того, что их маленький вклад внесён в Реальное Дело и два года жизни потрачено на отладку движения влево-вправо третьего заднего манипулятора робота, исследующего спутник Юпитера. И им пофиг, что работа камнетёса нудная и трудная.
Есть люди, которые фанатеют от того, что Скала, свежая жабоскриптовая библиотека и "делай что хочешь". И им пофиг, что результаты их многолетней работы предназначены для заказа по интернету кошачих лотков. (Естественно, те результаты, которые не ушли в мусорную корзину.)
Это совершенно ортогонально качеству работника.
Но, обычно, у программистов есть жёны и дети, потому хорошие уходят туда, где платят больше. И находят своё призвание в интеллектуальном анонизме на крутые языки программирования.
no subject
Date: 2016-02-11 10:28 pm (UTC)no subject
Date: 2016-02-11 10:35 pm (UTC)no subject
Date: 2016-02-12 02:24 pm (UTC)no subject
Date: 2016-02-12 02:27 pm (UTC)вам может тоже
Date: 2016-02-12 02:27 pm (UTC)Про ёжика в тумане, зазнайство, языки программирования
Date: 2016-04-18 02:06 am (UTC)