Нанодрама

Руководствуясь великими образцами литературы, шла она к победе любви через боль и страдания. Но герои её романов всегда сбегали задолго до финала.

Про ёжика в тумане, зазнайство, языки программирования и вериги

В гости к ivan_gandhi пришли perdakot, thedeemon, nponeccop и другие высоколобые товарищи, пообсуждать, почему это в области надёжного автомобильно-самолётно-спутникового софтостроения дремучие менеджеры нагораживают ООП с процессами и запрещают применять всякую красоту вроде
fun evenSqares {n:nat | n % 2 == 0 && n >= 4 %% n != 10}(x : int n) : int(n*n) = x*x

Выяснилось, что народ не знает различия между верификацией и валидацией.

Я их вечно путаю, так что объясняю просто: Та, которая «ве», - она про «Кто виноват?», а которая «ва», она про «Что делать?» (Кто не застал уроков литературы советских времён, пусть придумает что-то посовременнее.)

Верификация нужна для того, чтобы программисты не наделали ошибок, не выдумывали «более лучшие решения, потому что знаем мы этих идиотов, не понимающих великого PHP», а запрограммировали то, что приказано. Верификация работает с моделями и проверяет, чтобы они были воплощены правильно.

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

Качество верификации определяется метриками надёжности типа наработки на отказ. И стоимость растёт экспоненциально при приписывании сзади очередного нуля.

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

Mission critical - это то, где за ошибку можно получить не только штраф, но и конкретный уголовный срок. Особенно, если ошибки стоят не только кучу денег, но ещё и человеческие жизни.

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

При этом всё равно идут изменения в спецификацию по мере нахождения ошибок (в том числе, после тестирования) или получения новых указаний. И каждое изменение проходит полный цикл проверок. По этой причине любимые теоретиками и веб-разработчиками методы, советующие сначала делать, а потом думать, в таких проектах не проходят.
( Read more... )