Не уверен, рассказывал я об этом, или нет, но вот эти любимые некоторыми товарищами строгое доказательство корректности программ/алгоритмов, Agda, зависимые типы и так далее видится мне довольно бесполезной затеей. А также я давно перестал внимать рассуждениям таких же товарищей в стиле «MongoDB плохая база данных, потому что читай Афира » или «Ай-яй-яй, в Cassandra таймстэмпы вместо CRDT». Далее я постараюсь объяснить, почему так. А вы, как обычно, прочитаете по диагонали, выдерите слова из контекста и напишет в комментариях, что я ничего не понимаю 🙂

Как говорят в подкасте Разбор Полетов , «технология идеальна, а люди — чудаки». В мире, где программы пишутся роботами для других роботов, все алгоритмы имеют строгое доказательство корректности и в коде никогда не бывает багов. К сожалению, мы живем в мире, где программы пишутся людьми для других людей. А людям не нужно, чтобы программа имела доказанную корректность. Им нужно, чтобы в большинстве случаев все работало.

Не верите? Полистайте новости, посмотрите, сколько уязвимостей каждый месяц находят в браузерах, операционных системах, SSL или том же WordPress. Насколько мне известно, еще никто не перестал пользоваться MacBook’ами , iPhone’ами , или там Telegram’ом , потому что в них есть баги и уязвимости . Потому что в большинстве случаев все работает хорошо, и это главное. Языки Java и Python много лет сортировали данные неправильно , и этого никто не замечал. В MySQL есть эпичный баг про некорректную работу триггеров, который остается незакрытым вот уже 10 лет, но это никак не влияет на популярность MySQL. Более того, при создании новой системы заказчик приходит и прямо говорит, мол «я хочу, чтобы программа работала 99.999% времени». В такой постановке программа может 5 минут в год вообще не работать, с согласия заказчика .

Почему так происходит? Просто создавать доказано корректные программы слишком дорого, долго и непонятно, кому это поддерживать. В общем и целом, непрактично. Вот представьте, вы работаете над новым проектом два месяца. К вам подходит ПМ, и просит показать, что сейчас готово. А вы такой, мол «показать пока что нечего, я как раз почти доказал лемму, которая позволит мне доказать корректность уже второго по счету компонента системы». Вы ведь уже знаете, что будет дальше, правда? Скорее всего, вас просто заменят на того, кто способен за месяц сделать что-то более-менее рабочее. Вот поэтому мы и пишем системы, которые работают большую часть времени . Программисты довольны, потому что можно не напрягаться. Пользователи довольны, потому что получают продукт. Заказчик доволен, потому что получает прибыль. Все и всем довольны, жизнь прекрасна и удивительна.

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

Вообще, многие алгоритмы по своей природе имеют вероятностный характер, взять ту же область ИИ, всякие там Gossip, сетевые протоколы, например, DNS, и прочие. Тот же ИИ полон эвристик, зачастую вообще не имеющих за собой какого-либо обоснования, кроме опыта. Но мы говорим, что эти алгоритмы работают, потому что, будучи правильно примененными, они работают с достаточно большой вероятностью. Если ваша программа использует DNS, поздравляю, она не работает. Во всяком случае, далеко не в 100% случаев. Но это не означает, что программа не полезна и не работает в большинстве случаев. Вспомним также, что UUID, вообще-то говоря, можно случайно сгенерировать одинаковые, а в хэшах бывают коллизии. Просто такое случается редко. На самом деле, есть ненулевая вероятность случайного изменения битиков в памяти , даже при использовании ECC. Получается, что в действительности все алгоритмы — вероятностные .

В примере с теми же базами данных. Вот, считается, что Riak правильный. Если использовать CRDT, то данные никогда не потеряются и в конечном счете всегда к чему-нибудь сойдутся. Но что, если у меня одновременно сгорят три машины, со всеми шардами по некому ключу? Это не такой уж маловероятный сценарий, как вам может показаться. Во-первых, известно, что некоторые сервера, будучи введенными в эксплуатацию одновременно, любят также почти одновременно и выходить из строя. Во-вторых, в облачном хостинге, например, AWS , нельзя узнать, не запущены ли три виртуалки на одной физической машине. А если и можно, в Riak все равно нет rack awareness, чтобы в этом случае разнести данные по разным физическим машинам. Да и пожары в ДЦ никто не отменял. То есть, на самом-то деле, Riak теряет данные . Только делает это с маленькой вероятностью. И потому мы говорим, что вроде как и не теряет вовсе. Правда, удобно?

А давайте представим, что мы разрабатываем систему торговли ценными бумагами. Есть база с какими-то данными, например, котировками. Происходит нетсплит. PACELC (он же «CAP-теорема») недвусмысленно говорит, что в случае нетсплита можно либо послать пользователя нафиг, либо вернуть какую-то фигню. В случае с котировками, если по-честному, ни то, ни другое не является допустимым решением. Либо падать один раз в 3 дня, либо делать вид, что все ОК, хотя на самом деле ничего не ОК. Если выбирать между выйти из бизнеса и обмануть пользователя, разумеется обманываем пользователя! По-умному это сейчас называется «AP-системы» и «eventual consistency».

Другое фундаментальное ограничение — это скорость света. Я покупаю ценные бумаги по какой-то цене, которую я вижу в терминале. Но пока мой запрос летит до сервера, цена уже успела поменяться. Отклонить запрос нельзя, так как цена постоянно меняется. В этом случае система вообще не будет работать. Поэтому мы просто создаем иллюзию, что все хорошо, совершая покупку по цене, актуальной на момент получения запроса. На самом деле, эта цена тоже уже протухла, потому что прямо в этот момент от контрагента по TCP летит совсем другая цена.

Вот еще большая проблема. Что делать, если пользователь посылает запрос на запись, не дожидается ответа, и шлет этот же запрос повторно? Частично проблему позволяет решить прикручивание кэшика с ответами на последние выполненные запросы. Но что, если первый запрос был выполнен на 42%, после чего машина, на которой он выполнялся, взяла и сгорела? База данных оказывается в неконсистентном состоянии. Прикручивать ради этого случая распределенные транзакции ? Очень ресурсоемко (а следовательно и дорого), сложно в разработке и поддержке, при использовании микросервисов вообще практически нереализуемо.

Единственное известное мне универсальное решение заключается в том, чтобы писать код так, чтобы он мог отдать что-то правдоподобное даже в случае, если в базе записана ерунда. По-умному это сейчас называют robustness principle . Если же наша программа «не шмогла», ничего страшного, отдаем пользователю ошибку, пишем стектрейсы и прочие отладочные данные в лог, сбрасываем стейт, перезапускаем актор, дергаем алерт. Может быть, во второй или третий раз повезет больше. Все равно никакая строгая типизация и тестирование не найдут всех-всех-всех ошибок в системе. Особенно если эта система распределенная. Особенно если учесть, что в ближайшие 10 лет баг может ни разу и не проявиться. Стоит ли тратить на него время? По-умному это называется «принципом let it crash».

Проблема на 100% рабочих и доказанных решений усугубляется еще и тем, что доказательства справедливы для каких-то моделей . Но не факт, что ваша система соответствует этой модели. Вот возьмем самолеты. Они же вроде как летают, верно? При этом в основе лежит прочная теоретическая база и десятилетия инженерного опыта. Но на практике в воздухе с самолетом происходит множество событий, не предусмотренных моделью. Кроме того, нельзя полностью исключать человеческий фактор. Так или иначе, к сожалению, самолеты иногда разбиваются. К счастью, случается это не часто.

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

В теории теория ничем не отличается от практики. На практике имеем дело с живыми людьми, а следовательно и ошибками в коде, авралами, дэдлайнами, а также прочими унаследованными кодами. Мы сталкиваемся с факапами из-за человеческого фактора практически каждый день. При этом мне лично до сих пор еще ни разу не выпадала удача видеть в бою такое вот хитрое разбиение сети, чтобы прям ровно посередине, при котором MongoDB как-то там не совсем правильно себя ведет или Cassandra может (это еще от приложения сильно зависит!) неправильно смержить данные по таймстампам в столбцах. Какие еще нетсплиты, если человеческий фактор уничтожит все данные сто раз пока мы этого нетсплита дождемся? Когда и если такое случится, в крайнем случае восстановимся из бэкапа.

С учетом всего вышесказанного запишем определение:

Программирование — искусство заставить пользователя поверить, что куча костылей, подпорок и прочих «AP-решений» работают хорошо и что все под контролем.

Боритесь с перфекционизмом и помните, что код должен быть простым!

Дополнение: Судя по комментариям, даже когда люди не выдирают слова из контекста и читают не по диагонали, они додумывают что-то, чего в тексте нет. Поэтому поясню, что я вовсе не призываю вообще не проверять корректность программ. Скорее я призываю делать это простыми и понятными способами, как, например, написанием как можно более простого и понятного кода, строгой статической типизацией, высокоуровневыми безопасными языками с автоматической сборкой мусора, проверками на выход за границы массивов и так далее, различного рода санитайзерами и статическими анализаторами, в том числе флагами компиляторов вроде -Wall , дотошным code review, а также автоматическими тестами, кучей автоматических тестов, не исключая property based . Поскольку программы не бывают на 100% рабочими, на практике достаточно чего-то в районе 99%. Добивать остальное — слишком ресурсоемко и 100% вы все равно никогда не достигнете. По отношению к стороннему софту, тем же БД, это также применимо.