Почему земляне делают глючный софт и железо

Думаю никто не станет спорить с тем, что качество сколь-либо сложных систем создаваемых землянами далеко от идеала. Конечно, можно сказать, что всё работает — самолёты летают, космические корабли бороздят просторы орбиты Земли и т.д.

Но при этом все привыкли к тому, что ПО на их устройствах работает непредсказуемо, через раз, что даже установка самых последних обновлений не гарантирует отсутствия проблем с безопасностью, что часто в открытом, массово используемом коде находят ошибки существующие там много лет, что даже у крупных и «технологических» компаний бывают сбои и утечки данных, что космические аппараты разбиваются или теряют часть функциональности вовсе не из-за козней инопланетян (марсиане клянутся что не сбивали ExoMars).

Хотелось бы рассмотреть причины и возможные пути решения этой планетарной проблемы.

1. Непрофессионализм и некомпетентность исполнителей — земляне, в основной массе, не научены и не приучены делать свою работу хорошо. Эта проблема стоит очень остро, и говорить о ней можно долго, но видимо надо писать отдельный пост. Тут лишь можно сказать, что настоящие профессионалы всё-таки есть, на передовые проекты должно хватать, но проблемы есть и в таких проектах, значит дело не только в этом.
   
   
2. Отсутствие цели сделать хорошо/плохой менеджмент/недостаточные инвестиции — эта причина вполне вероятна в обычных коммерческих проектах, где задача стоит получить краткосрочную прибыль, а не сделать хорошо. Но это явно не про космические проекты, где цена ошибки слишком велика и в деньгах и в репутации, а затраты на разработку по некоторым оценкам в 160 раз выше обычной коммерческой разработки, однако также без гарантии надёжности.
   
   
3. Использование неподходящих инструментов/попытка молотком шлифовать линзу — вот эта причина мне кажется главной и о ней я буду говорить далее. Именно из-за неправильного подхода к решению задач честные программисты никогда не говорят «Да, оно работает», а говорят «Вроде работает», «Должно работать».

Когда земляне берутся за самые сложные из стоящих перед ними задач, вполне логично было бы применять для их решения самый лучший из имеющихся инструментов.
И этот инструмент, это точно не человеческий мозг, мозг homo sapiens это как раз инструмент из серии «вроде работает» и не стоит этому удивляться, всё-таки эволюционировал он для совсем других задач, поэтому даже самый крутой профессионал может сделать тупую ошибку по куче причин.

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

Чтобы понять, что это за волшебный инструмент стоит попробовать ответить на вопросы вроде «Почему небоскрёбы не разрушаются под своим весом или на ветру?», «Как наши космические аппараты добираются до цели в необъятных просторах космоса?», «Как мы умудряемся надёжно пересылать данные по ненадёжным каналам связи?», «Откуда взялись надёжные методы шифрования?» и так далее и тому подобное.

Ответ на все эти вопросы один, этот инструмент — математика. Математика это магия современного мира, для непосвящённых такие артефакты как Zcash или CryptDB, да и, ставшее привычным, асимметричное шифрование выглядят как волшебство, хотя это лишь применение этого мощного инструмента.

Для того, чтобы сказать — «Да, программа работает как требовали», надо иметь математическое доказательство этого утверждения, к сожалению я не специалист в этой сфере, но насколько знаю процесс этого доказательства достаточно сложный, но это не должно быть препятствием по следующим причинам:

1. Иного пути нет, наши системы усложняются, новые слои опираются на страрые, но к сожалению это не очень надёжный фундамент.
   
   
2. Доказывать нужно небольшие программы (юникс-вей).
   
   
3. Доказывать нужно лишь программы критичные для безопасности надёжности. Можно не доказывать корректность офисного пакета, но микроядро ОС или библиотеки шифрования должны быть доказаны.
   
   
4. Доказывать не обязательно существующий универсальный софт, не обязательно это будет ОС общего назначения, возможно что-то более простое, без свистелок, но максимально надёжное для медицины, транспорта, АЭС.
   
   
5. Использование строго математических языков программирования может снизить затраты на доказательство (Haskell?). Да, они могут быть в чём-то сложнее обычных ЯП, но их сложность соответствует сложности задач которые необходимо решать.
   
   
6. Не обязательно доказывать сразу всё, но шаг за шагом можно построить доказанную инфраструктуру для построения надёжных систем.

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

Думаю все хотели бы, чтобы на АЭС, в медицинском оборудовании и подобных местах работало абсолютно надёжное ПО.

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

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

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


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

Думаю, для того чтобы земная цивилизация устойчиво развивалась ей пора задуматься над надёжностью своей инфраструктуры, касательно ИТ мне это видится так — нужно выбрать/создать высокоуровневый математический язык программирования и начать создавать полностью на нем (без спрятанных под капотом сишных либ) наиболее критичные программы с последующим их доказательством. Вполне вероятно, что и аппаратная архитектура процессоров должна быть доказана и заточена под исполнение программ на таком языке (лисп-машины?).

Кто это должен делать? Не знаю, но такой же вопрос можно было бы задать на предложение всем миром писать ядро ОС, однако Linux вполне пишут, а значит варианты есть. Есть например формально верифицированное ядро seL4 (пояснения в их вики) разработанное в NICTA, если подобные проекты на станут основой для цифровой инфраструктуры будущего, то у человечества появятся шансы не пройти великий фильтр цивилизаций (кто уверен что вирус не начнёт ядерную войну?).

ОБНОВЛЕНИЕ: В процессе обсуждения в комментариях созрела важная мысль — для того, чтобы внедрять в критичных сферах верифицированное ПО вовсе не обязательно останавливать текущую разработку, нужно параллельно создавать свободные верифицированные компоненты, а по их готовности новые вещи делать с их помощью, например вышеупомянутое микроядро seL4 для встраиваемых нужд уже есть, а значит нужно его использовать везде где он подходит. И работать над другими компонентами.