vit_r: default (vit_r)
[personal profile] vit_r
Software Engineering
В гости к [livejournal.com profile] ivan_gandhi пришли [livejournal.com profile] perdakot, [livejournal.com profile] thedeemon, [livejournal.com profile] nponeccop и другие высоколобые товарищи, пообсуждать, почему это в области надёжного автомобильно-самолётно-спутникового софтостроения дремучие менеджеры нагораживают ООП с процессами и запрещают применять всякую красоту вроде
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», наглядно показала, что бывает, если экономить на «устаревших методологиях».

Date: 2016-02-11 03:22 am (UTC)
From: [identity profile] pappadeux.livejournal.com
верификация

Date: 2016-02-11 06:35 am (UTC)
From: [identity profile] vit-r.livejournal.com
Спасибо, исправил.

Date: 2016-02-11 04:17 am (UTC)
From: [identity profile] thedeemon.livejournal.com
У меня там в одной строчке две опечатки. :) Должно быть
fun evenSquares {n:nat | n % 2 == 0 && n >= 4 && n != 10}(x : int n) : int(n*n) = x*x

>...позволяют людям, не хватающим звёзд с неба, производить такой софт, что космические аппараты не заваливают миссии, ракеты не взрываются, самолёты не падают, поезда с рельс не сходят и машины не разгоняются, когда надо тормозить.

Тут стоило добавить "обычно". А то ведь регулярно и заваливают, и взрываются (каждая десятая или около того), и бороздят просторы мирового океана.

Date: 2016-02-11 05:39 am (UTC)
From: [identity profile] perdakot.livejournal.com
> каждая десятая или около того

Может заплатить за неудачи все же дешевле-выгоднее, чем нанимать "хватающим звёзд с неба" и долго верифицировать? А людей новых нарожают, тем более что от долгой верификации люди тоже могут умереть, не дождавшись вертолета или светофора.

Date: 2016-02-11 06:31 am (UTC)
From: [identity profile] vit-r.livejournal.com
В России мало когда что делают по инструкции. В Японии мало когда задумываются о том, что инструкция не правильна.

А ракеты заваливаются в основном не из-за программистов, а из-за того, что им техзадание неполное дали. В том числе и со знаменитым Арианом.

Date: 2016-02-11 07:38 am (UTC)
From: [identity profile] izard.livejournal.com
Давно хотел написать подобный пост, упомянув товарищей из списка и IEC61508 :) Последние 2 абзаца вообще бы почти дословно так и сформулировал ж)

Date: 2016-02-11 08:11 am (UTC)
From: [identity profile] vit-r.livejournal.com
Все знают. Все молчат. Мне одному отдуваться. :-D

Date: 2016-02-11 11:17 am (UTC)
From: [identity profile] izard.livejournal.com
У вас материал круче - космические технологии. Про мои станки или транспорт всегда можно сказать со стороны - "не понимают своего счастья, но там и задачи плевые"

Date: 2016-02-11 07:56 am (UTC)
From: [identity profile] veremeenko-alex.livejournal.com
>fun evenSqares {n:nat | n % 2 == 0 && n >= 4 %% n != 10}(x : int n) : int(n*n) = x*x

Мода на такое - потому что веб! Ну упало, ну хрен с ним.

А стоит хоть краешком прикоснутся с реальным миром, хоть одним датчиком - и все приехали: лезут погрешности, датчик может подвирать, зависимости мало что нелинейные да еще и дырками.

Date: 2016-02-11 10:26 am (UTC)
From: [identity profile] thedeemon.livejournal.com
Это пять.
Какая мода? Тот язык знают полтора человека.
Какой веб? Ни я, ни пользователи того языка вебом не занимаются. В вебе такое не применяется.
Какой упало? Такие программы как раз не падают (при работающей аппаратуре, конечно).
В условиях реального мира и датчиков агитируете за говно и палки вместо математики?

Date: 2016-02-11 10:32 am (UTC)
From: [identity profile] vit-r.livejournal.com
Математика не знает о несовершенстве мира. В этом основаная проблема функционального подхода.

Date: 2016-02-11 10:48 am (UTC)
From: [identity profile] thedeemon.livejournal.com
А кто знает? И в каком виде существует это знание, почему оно невыразимо языком математики? М-ка это же язык.

Date: 2016-02-11 11:02 am (UTC)
From: [identity profile] vit-r.livejournal.com
Инженеры и физики знают.

Во многих случаях "теоретическое" решение слишком сложно. Особенно, если в системе слишком много связей. Например, есть случаи, когда правильно использовать таблицы вместо формул.

Date: 2016-02-11 01:40 pm (UTC)
From: [identity profile] gineer.livejournal.com
Не поверит же. :) Идеалисты не верят в практику.

Date: 2016-02-11 05:25 pm (UTC)
From: [identity profile] thedeemon.livejournal.com
Не-не, тут я с vit_r полностью согласен.

Date: 2016-02-12 02:27 pm (UTC)

вам может тоже

Date: 2016-02-12 02:27 pm (UTC)
From: [identity profile] gineer.livejournal.com
реквестируется комментарий к http://ivan-gandhi.livejournal.com/3493149.html?thread=57333789#t57333789

Date: 2016-02-11 05:00 pm (UTC)
From: [identity profile] pappadeux.livejournal.com
> А кто знает?

Э?!

Инженеры знают

Это, вообще говоря, прямая обязанность инженера - в его области знаний и умений ЗНАТЬ И ПОНИМАТЬ несовершенства мира сего...

Date: 2016-02-11 01:28 pm (UTC)
From: [identity profile] gineer.livejournal.com
а еще это -- http://oleyka.livejournal.com/96939.html

Date: 2016-02-11 03:44 pm (UTC)
From: [identity profile] vit-r.livejournal.com
Полтора.

Date: 2016-02-11 09:09 pm (UTC)
From: [identity profile] anonim-legion.livejournal.com
>позволяют людям, не хватающим звёзд с неба,

Причина, по которой там оказываются такие люди, как-то не описана. Но как-то раз в этом блоге встречалось нечто вроде "стали заниматься серьёзными(!) делами, а не сбежали за деньгами в стартапы". Серьёзными, Карл!

Date: 2016-02-11 09:35 pm (UTC)
From: [identity profile] vit-r.livejournal.com
http://vit-r.livejournal.com/13500.html

Тут такое дело...

Есть люди, которые впадают в экстаз от того, что их маленький вклад внесён в Реальное Дело и два года жизни потрачено на отладку движения влево-вправо третьего заднего манипулятора робота, исследующего спутник Юпитера. И им пофиг, что работа камнетёса нудная и трудная.

Есть люди, которые фанатеют от того, что Скала, свежая жабоскриптовая библиотека и "делай что хочешь". И им пофиг, что результаты их многолетней работы предназначены для заказа по интернету кошачих лотков. (Естественно, те результаты, которые не ушли в мусорную корзину.)

Это совершенно ортогонально качеству работника.

Но, обычно, у программистов есть жёны и дети, потому хорошие уходят туда, где платят больше. И находят своё призвание в интеллектуальном анонизме на крутые языки программирования.

Date: 2016-02-11 10:35 pm (UTC)
From: [identity profile] vit-r.livejournal.com
Скоро полночь, руки уже постепенно отключаются от головы.

Date: 2016-02-12 02:24 pm (UTC)
From: [identity profile] gineer.livejournal.com
реквестируется комментарий к http://ivan-gandhi.livejournal.com/3493149.html?thread=57333789#t57333789
From: [identity profile] livejournal.livejournal.com
User [livejournal.com profile] villmanstrand referenced to your post from Про ёжика в тумане, зазнайство, языки программирования и вериги (http://villmanstrand.livejournal.com/720051.html) saying: [...] Оригинал взят у в Про ёжика в тумане, зазнайство, языки программирования и вериги [...]

Profile

vit_r: default (Default)
vit_r

February 2026

S M T W T F S
12 34 567
8 91011121314
15161718192021
22232425262728

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Feb. 10th, 2026 05:31 pm
Powered by Dreamwidth Studios