17 декабря 2016 в 20:54

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

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

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

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

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

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

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

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

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

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

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

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

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

  2. Доказывать нужно небольшие программы (юникс-вей).

  3. Доказывать нужно лишь программы критичные для безопасности надёжности. Можно не доказывать корректность офисного пакета, но микроядро ОС или библиотеки шифрования должны быть доказаны.

  4. Доказывать не обязательно существующий универсальный софт, не обязательно это будет ОС общего назначения, возможно что-то более простое, без свистелок, но максимально надёжное для медицины, транспорта, АЭС.

  5. Использование строго математических языков программирования может снизить затраты на доказательство (Haskell?). Да, они могут быть в чём-то сложнее обычных ЯП, но их сложность соответствует сложности задач которые необходимо решать.

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

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

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

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

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

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

Дятел? Причём здесь дятел
Это старый мем: «Если бы строители строили дома как программисты пишут программы, то первый залётный дятел разрушил бы цивилизацию»

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

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

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

— Это чудо… чудо! О, как великолепно!

— Да. Это самое прекрасное из того, что я только видел во Вселенной…

— Наверное, планеты и существуют для того, чтобы распуститься только один раз… Но разве этого мало?..

«Когда расцветают бомбы» Роджер Желязны Сергей Битюцкий

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

Комментарии (306)

  • +3
    К сожалению, наводить порядок в говнокоде и тем более разрабатывать инструменты, исключающие появление говнокода — сейчас не в тренде и невыгодно. Всем надо подешевле, побыстрее, а ещё лучше — если код напишет кто-то другой (та же нейросеть). Ну так и получается, что иногда происходят катастрофы по вине плохого кода, плюс неэффективное расходование ресурсов.
    Что должно случиться, чтобы приоритеты поменялись и математически доказанные программы вошли в моду?
    • –4
      Думаю что тут необходимо влияние государства (групп государств) на бизнес, нужно выработать стандарты, которые не позволят в критических местах использовать плохокод.
      Сегодня же есть какие-то процедуры сертификации, например, самолётов, нужно их сделать более строгими.
      • +4
        И в результате получить еще одну бюрократическую цепочку и сделать софт дороже.
        • 0
          Да, но надо ли экономить на том что может стоить жизни или жизней?
          • +1
            Смотря с какой точки зрения смотреть, с экономической стоит, тут у нас чистая статистика.
            • –2
              Кто это считал? Представим на минутку что из-за вируса весь цивилизованный мир оказался без электричества на неделю, какие будут убытки?
              • +5
                Теперь умножаем эти убытки на вероятность такого события, получаем изчезающе малую величину и спим спокойно. Вы ведь не ходите в каске от метеоритов?
                • +2
                  А как вы вычислили вероятность такого события?
                  Как та индейка у Талеба, которая думала что раз меня каждый день кормят, то так будет всегда, а вероятность казни топором исчезающе мала?

                  В каске не хожу, но считаю что противоастероидную систему для планеты разрабатывать нужно.
                  • +2
                    Тут не особо важна какая вероятность события, тут важнее, что не ее ПОЛНОЕ устранение у вас тупо не хватит ресурсов. Грубо говоря, вам тогда надо заняться защитой каждого индивидуума от метеоритов мегатонного класса. Справитесь?
                    • 0
                      я не про индивидуальную защиту, я про защиту от катастроф, на голову может упасть и мелкий камень, от такого нам пока не по силам защититься, но не допустить падения таких, что могут вызвать ядерную зиму мы обязаны.
                      • +2
                        пока по-крупному не долбанет, деньги не перенаправят. увы, пока экономически выгоднее делать код без гарантий (почитайте любое eula) и нет реальной ответственности, будет все как есть. как только станет невыгодно класть на критичный код, сразу найдут / придумают средства, даже если это на порядок замедлит работы. если непонятно, что и почему происходит, всегда дело в деньгах
                        • +3
                          Причем, резко вырастет не только время разработки, но и стоимость единицы времени. Если разработчик будет нести личную ответственность, материальную или уголовную, то придется уравновешивать это чудовищными зарплатами. И то не факт, что на это согласятся хорошие специалисты, а не халявщики, которые будут надеяться на удачу.
                          • +2
                            Стоимость не должна сильно изменится. Посмотрите на медицину. Многие медики несут личную, в том числе и уголовную ответственность. А зарплаты так себе.
                            • +1
                              Только за совсем уж явные косяки. Многочисленные ошибки в диагнозе не считаются. В США от врачебных ошибок погибают более 200 тысяч человек ежегодно. И хочу отметить, что профессия врача в США оплачивается очень хорошо.
                              • 0
                                Явные косяки? Возьмем к примеру анализы — ошибка в определении группы крови может привести к смерти пациента. Ошибочный анализ на генетическую совместимость пары может привести к рождению неполноценного ребенка.
                                И то и другое выполняется на потоке… То есть сидит человек и выдает по нескольку анализов в день. И за каждый подписывается.
                                В Челябинске, например, за такую работу платят от 15 (в гос лабораториях) до 30 (в частных) т.р.
                                • 0
                                  Ни один человек не согласиться работать так, что совершая действия, в правильности которых он полностью уверен на момент их совершения, иметь возможность потом за это огрести.

                                  Ответственность возможна только за отклонения от инструкций и норм. Там, где есть элемент творчества и работа интуиции (у тех же медиков — постановка диагнозов), ответственности нет.
                                  • 0
                                    Ну вы хоть погуглите. Много случаев когда возбуждаются уголовные дела за неправильный диагноз повлекший за собой смерть пациента.
                                • +1
                                  А местный терапевт на любой кашель штампует «ОРЗ/ОРВИ».

                                  Возьмем, к примеру, близкую для меня ситуацию — ГЭРБ, который проявлялся в постоянном кашле. Мне пришлось пройти около пяти обследований, дважды полежать в стационаре, прежде чем врачи поставили правильный диагноз. В перспективе ГЭРБ имеет высокие шансы привести к раку пищевода. И я уверен, что если бы дело дошло до рака, то никто из врачей, ставивших мне раз за разом неправильный диагноз, не понес бы ни уголовной, ни административной, ни даже финансовой ответственности.
                                  Если же рассматривать не только смерть, но и инвалидность или получение перманентных последствий от неправильного лечения, то количество косяков вырастет на порядок.

                                  Это я не к тому, что врачей нужно обязательно привлекать, а к тому, что в их работе косяки являются следствием характера и уровня организации самой работы. Иногда это приводит к смерти или инвалидности пациента. Но без врачей этих самых смертей и инвалидностей было бы на порядки больше.
                                  • 0
                                    Вам не повезло с врачами, у меня же оба раза, когда я обращался к ЛОРу с больным горлом после непродолжительного лечения отправляли к гастроэнетрологу.
                          • +2
                            ну, скажем так, ряды этот подход прорядит. соответственно вырастет цена работников. но тут еще скорее всего ужесточится отбор всякими сертификатами и т. д. ведь приятно, конечно, если человек несет ответственность, но даже если его расстрелять, миллиарды, вложенные в спутник не вернешь. скорее всего, есди сегмент «доказательного программирования» и появится, будет он ничтожной каплей в море.
                            касательно медиков — судя по договорам, какие я подписываю на всяких анализах и процедурах — это типа той же eula. чтобы медработник реально понес ответственность за что-то а) я должен быть депутатом или человеком с баблом, б) медработник должен сильно насолить коллегам, так, чтобы они захотели его слить.
                  • +1
                    Точно также как вы вычислили вероятность падения метеорита на голову и потому приняли решение не носить каску. Точно также как вы вычисляете вероятность серьёзных проблем от мороза -30 и принимаете решение одевать шапку, а не рассуждаете о планетарной системе защиты от морозов зимой.
                    • –1
                      Вероятность падения метеорита на голову я рассчитать не могу, я просто ей пренебрегаю на свой страх и риск, этой мой выбор, от него не зависит судьба цивилизации.
                      А проблемы от мороза это не оценка неведомого, а вполне научные данные.
      • 0
        https://en.wikipedia.org/wiki/Technology_readiness_level

        Более строгими? У меня складывается впечатление, что вы не совсем понимаете, о чем пишите.
        • 0
          т.е. у них всё настолько хорошо что аварий из-за багов в ПО не бывает?
          • 0
            У кого у них? Вы сказали, что нужно выработать стандарты, я вам дал ссылку на стандарты. Потрудитесь объяснить, чем эти стандарты плохи, что в них вы хотите поменять и по какой причине.
            • +1
              Ну например у NASA или ESA, плохи они тем, что не защищают от потери космический аппартов из-за программных ошибок.
              • +1
                Дайте данные:
                1. Что не защищают.
                2. Какой процент потерь космических аппаратов происходит из-за программных ошибок и сколько это в денежном выражении (интересует именно процент потерь, обусловленный «программными ошибками», а не некорректными входными данными/данными с датчиков).
                3. Сколько будет стоить защита по вашей методике и какой от этого будет профит.

                Пока это балабольство какое-то. Все идиоты, один worldmind Д'Артаньян, который все лучше всех знает.
                • 0
                  Никого идиотами я не называл (и даже пояснил почему раньше этот путь не подходил) и честно сказал, что я не специалист, но из того, что я знаю и понимаю, логично вытекает описанное.
                  Исследований о проценте катастроф из-за багов в ПО не проводил, хотя думаю они есть (может lozga Zelenyikot Shubinpavel подскажут), вот несколько интересных случаев примеров.
                  Стоимость по тем же причинам точно оценить не могу, но тут приводил пример, вроде не такие уж астрономические затраты и вполне возможно что их ещё можно снизить повысив уровень автоматизации.
                  • +2
                    Собственно все ошибки из-за ПО что я вспомнил произошли из-за того, что просто не были в свое время учтены все обязательные правила при разработке систем. Просто не было сил, денег или времени чтобы прогнать все необходимые тесты на модели аппарата.
                    Исключения, только очень старые истории вроде компьютера Аполло которые не успевал обработать поступившие команды

                    При этом, си языки используются редко. Из тех, что я знаю, там больше наследников Паскаля. Например в США язык Ада, а у НПО Решетнева Модула-2.
                • +1
                  > Пока это балабольство какое-то. Все идиоты, один worldmind Д'Артаньян, который все лучше всех знает

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

        Давайте, я расскажу, что будет: самолеты продолжат падать, электричество отключаться, а метеориты падать на головы, но появится новая бюрократическая структура, которая съест часть налогов.
        • 0
          С чего это новая? Хватит тех чьто есть сейчас, а может и меньше понадобится.
    • 0
      Более того, говно код прибыльней качественного кода, так как дешевле в написании, и можно бесконечно собирать деньги с пользователей за починку бесчисленных багов и продаже поддержки которая будет героически заставлять его работать.
      • +1
        Есть завод, он производит, технически сложные штуки. Если он получит софт (пусть глючный и падучий), он сможет заптимизячить свои штуки (с геморроем, шутками и прибаутками, матами и т.д., но сможет) и на этом будет экономить олимпиард денег в год. Спросите у директора завода, хочет ли он получить такой софт сегодня, но с глюками или через год без глюков.

        Я не сторонник говнокода, но реальность такова, что все хотят получить хоть как-то работающий софт сегодня и согласны им пользоваться пока вы его до завтра доработаете, а не сидеть и ждать до завтра, а то и до послезавтра, пока вы там все протестируете.
    • +1
      Почему к сожалению? Говнокода ровно столько, сколько нужно экономике. Если вдруг окажется что говнокод уменьшает её эффективность, она начнёт больше инвестировать в нормальный код. Конечно всем бы нам хотелось получать максимально быстро новые качественные вещи за небольшие деньги, но это утопия.
      • +1
        Ну тут получается маленькая проблема. Пока востребовано много говнокода, появляется много программистов соответствующего уровня. Будет как с микроскопом, превратить его в молоток на порядки проще, чем из молотка сделать оптический прибор. Все же переучивать человека выйдет скорее долго и дорого, а если еще и не у всех результат будет положительным…
        P.S. Нынче зачастую купить качественную вещь непросто, даже имея приличные деньги. Просто потому, что их не деают массово, а единичные «ручные» стоят совсем уж неприлично.
        • 0
          Будет как с микроскопом, превратить его в молоток на порядки проще, чем из молотка сделать оптический прибор

          Кривая аналогия. Изначально у вас на руках не микроскоп и даже не молоток, а просто кусок камня — люди не рождаются профессиональными программистами.
          • 0
            Вовсе нет. Камень получается уже огранен годами обучения и работы. Нет в некоторых пределах пластичность остается, но они не всегда достаточно большие.
            Пожалуй приведу другой пример — столяр или плотник, вроде как оба работают с деревом. Но сможет ли тот, кто всю жизнь делал дома, вдруг сразу художественно вырезать орнамент на шкатулке? Или наоборот, всю жизнь делая художественные поделки, внезапно взять топор и так же быстро и качественно поставить баню?
            Вот и выходит, даже если конкретный человек запросто переучится на «новые рельсы», это не обязательно случится быстро для всей отрасли. Отчего попытки изменить подход к делу выйдут просто чудовищными по затратам, если пытаться сделать это «мгновенно». А если добавить поговорку про «слабое звено» помноженную на текущий зоопарк решений, становится воистину печально.
      • 0
        Вы гистерезис не учли
    • +2
      По моему, многим разработчикам просто не хватает образования, что бы понять такой подход (я как-то пробовал прочитать школьникам краткий курс Haskell и обнаружил что они не понимают что такое множество). Они свое непонимание передают менеджерам, и те не уделяют внимания качеству как чему-то недостижимому.
      По этому я считаю, что надо всем, особенно программистам, учить математику (матлогику, алгебру, теорию категорий) — тогда внедрение верификации пойдет легче.
      • 0
        Если учить математику, то когда разбираться с собственно программированием? :)
        Современному программисту и так постоянно приходится разбираться с чем-то новым в программировании плюс — погружаться в новые предметные области: собственно что он программирует.

        Тут уж скорее нужно математикам не абстракциями рассказывать, которыми они в своей среде оперируют, а «опускаться» на уровень программистов и, грубо говоря, делать методички для не математиков. Пусть и с определённой подготовкой в виде курса математики в ВУЗе. Который они уже основательно подзабыли.
        А если спускать инженерам (в любой, кстати области) какую-то абстрактную математику, то и не будут они её использовать. Просто даже не поймут — как?
        И будут дальше делать: по наитию, как привыкли, как переняли у коллег…
        • +1
          Пора уже перестать спешить. Все равно в ближайшее время простой программист не сможет конкурировать с ИИ и/или дешевыми программистами из стран третьего мира.
          Правильно, если надо учиться на программиста не пять, а все десять лет, с глубоким изучением сложных абстрактных дисциплин. Искусственные нейронные сети с этим еще не скоро справятся, а компановать из готовых модулей скоро научатся.
        • 0
          Кодерам оставить просто программирование, а специалисты с высшим образованием должны думать о более сложных задачах.
          • +1
            А что значит «просто программирование»?
            • 0
              То программирование, которое не требует знаний математики
              • 0
                Откройте любую книгу по программированию — там какая-то специальная математика не особо-то нужна.
                Снизу доверху: от кодера до руководителя проекта.

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

                Вы каждый день интегралы по поверхности не берёте, а пользуетесь готовыми формулами, которые вам вывели математики.
      • 0
        Я как-то думал над тем, что должен знать программист с высшим образованием и надумал такой список, буду рад замечаниям и merge request'ам.
        • 0
          На мой взгляд просто обобщенный хороший программист (не только ученый) все-таки должен знать лямбда-исчисление и теорию категорий, основы криптографмм и блокчейна, и понимать что из себя представляет доказательство правильности.
          А вот последние 4 пункта из общиепрограммстких, и биоинформатика из «для ученых», на мой взгляд, слишком специфичны и не всем обязательны.
          Да, машинное обучение для ученых надо знать, но простые программисты могут его обойти стороной.
          • 0
            Да, биоинформатику только в трендах нужно оставить, представлению нужно иметь. А машинное обучение набирает обороты, надо заранее начать учить.
            • +1
              Я думаю, что в ML все еще много раз поменяется. Сейчас там практически одни нейронные сети. Вы правильно отметили, что они трудно верифицируются. По этому я жду появления/возраждения чего-то типа Индуктивного логического программирования. А может оно пойдет в сторону скрытых марковских моделей, или еще куда.
              • 0
                Да вот есть риск, что определённый класс задач решается только структурами а-ля мозг с присущими ему недостатками. Хотя я был бы рад если бы для них нашлись строгие решения.
          • 0
            На мой взгляд просто обобщенный хороший программист (не только ученый) все-таки должен знать лямбда-исчисление и теорию категорий

            А где в своей работе ему всё это применять?
            • 0
              Например, выучить язык, для понимания которого эта математика полезна, и писать на нем код.
              • 0
                А он сейчас пишет код и проектирует системы.
                На других языках.

                Зачем ему изучать некую специфическую математику с перспективой, что пригодится она только для того, чтобы изучить такой же специфический язык программирования?
                И много программистов, для которых программирование — профессия (деньги они этим зарабатывают) — много их станет изучать эту специальную математику, чтобы впоследствии въехать в такой же «математизированный» язык?
                • 0
                  Что бы софт становился более надежным.
                  Языки, не основанные явно на математике, не способствуют написанию надежного софта.
                  Да и в C++ то же виртуальное наследование хорошо описывается теорией категорий, и знающие ее сможет применять его более осмыслено.
                  • 0
                    Что бы софт становился более надежным.
                    Языки, не основанные явно на математике, не способствуют написанию надежного софта.

                    А в «языке основанном на математике» нельзя ошибку сделать?

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

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

                      На счет сотен тысяч программистов я сильно сомневаюсь.
                      • 0
                        Ну так в любом компилируемом языке программирования подавляющая часть ошибок ловится на этапе компиляции :)
                        • +1
                          Вы пробовали сравнивать?
                          • 0
                            Что с чем сравнивать? :)
                            • 0
                              Разные компилируемые языки на предмет доли нахйденых ошибок при компиляции.
                              • 0
                                Так тут и сравнивать нечего.
                                Ошибки, вылавливаемые компиляторами, это опечатки и нарушения синтаксиса. Это же очевидно :)
                                Логические и алгоритмические ошибки они не могут обнаружить: компилятор же не знает что именно имеет ввиду программист.
                                Хотя в С/С++ полезно читать предупреждения. Бывает за ними скрывается часть этих ошибок.

                                Может в «математических» языках более чётко поставлена работа с ресурсами и уменьшены другие возможности «выстрелить себе в ногу», но это же как я понимаю не благодаря их «математичности».
                                И в «вольных» языках если придерживаться известных техник программирования — можно уменьшить количество таких ошибок во много раз, если не извести совсем.
                                • 0
                                  На ассемблере никогда не писали? Там тоже можно придерживаться известных техник, чтобы совершать меньше ошибок.
                                  • 0
                                    На заре своего програмёрства было дело.
                                    Но техник особых не знал.
                                    • 0
                                      Сравнивая ассемблер и С++, язык влияет на количество ошибок в программе?
                                      • 0
                                        Программы очень разные.
                                        На ассемблере такие программы, как на C++ — замучаешься писать.
                                        На нём я не писал какую-то сложную обработку данных, пользовательский интерфейс.
                                        Они более… прямолинейные что-ли. Не очень много ветвлений, условий всяких. И более выверенные были.
                                        В общем, сложно сравнить.
                                • +1
                                  Опечатки и синтаксис это такая мелочь что и за ошибки считать не стоит. А вот перепутать переменные местами, или нечаянно в цикле изменить переменную-счётчик этого же цикла, или нечаянно изменить константу — такие ошибки вам ни один из обычных компиляторов не словит, разве что какой-то глубокий анализ нейронной сетью… а вот такие языки как Haskel, Rust и тому подобные не позволят сделать таких глупых ошибок не позволив даже скомпилировать программу.
                                  • +1
                                    … нечаянно изменить константу
                                    … такие ошибки вам ни один из обычных компиляторов не словит

                                    Серьёзно?

                                    перепутать переменные местами

                                    Это — да, хороший контроль.
                                    А как это в haskell'е сделано?

                                    А насчёт в цикле не изменить переменную-счётчик…
                                    Это будет покруче запрета goto :)
                                    • 0
                                      А как это в haskell'е сделано?
                                      Большим уровнем абстракции. Выбрать из коллекции элементы по фильтру, отсортировать, провести какие-то изменения в каждом отобранном элементе — и всё в одну строчку, где ошибиться сложнее, чем расписывая циклы через итераторы над коллекциями.
                                      • 0
                                        Не-не. Погодите.
                                        Функцию можно в хаскеле объявить? С 2-3 переменными одинакового типа? (типы же там есть? Он же жёстко типизированный язык?)

                                        И вот при вызове функции — можно вместо, грубо говоря, (x, y, z) передать (x, x, z) или (x, z, y)?
                                        • 0
                                          Эти ошибки компилятор не ловит.
                                          • 0
                                            Остаётся дождаться комментария от Alexeyslav — какое перепутывание переменных он имел ввиду.
                                        • 0
                                          Кстати, Rust в некоторых случаях передачу (x,x,z) вместо (x,y,z) отловит :-).
                                          Но в том то и дело, что такие функции прихолится объявлять не часто.
                                          У меня в Haskell несколько раз допускалась ошибка, которую пришлось дебажить, типа let n1 = n+1 in ..., где в… скописченый код, в котором я не все n заменил на n1. Ради таких случаев я даже выраьотал технику писать вместо let такую конструкцию case n+1 of n ->…
                                          • 0
                                            У меня в Haskell несколько раз допускалась ошибка, которую пришлось дебажить, типа let n1 = n+1 in ..., где в… скописченый код, в котором я не все n заменил на n1

                                            А n у Вас при этом тоже использовалось и оказалось того же типа, что и n1?
                                            • 0
                                              Использовалось, но не должно было. Несколько раз требовалось выполнить похожий код и для целого числа n, и для n+1, а выделять его в отдельную функцию было лень или не очень удобно. Пришлось изобретать способы маскировать старую версию переменной.
                                    • 0
                                      Именно. Потому что многие компиляторы идут на хитрость и константы на самом деле переменные, к которым запрещено напрямую обращаться. Или константы-объекты которые передаются в функцию по ссылке… и ничто не мешает коду внутри изменить этот объект при помощи манипуляций с указателями(напрямую-то компилятор ругнётся).

                                      Изменять счётчик цикла — это великое зло чреватое граблями, и да оно похуже использования goto… поэтому придумали такие штуки как итераторы, в которых нет доступа к этому счётчику и накосячить нереально. Но итераторы начинают проникать и в классические языки, но опять же как-то местами очень костыльно.
                                      • +1
                                        Речь была про:
                                        нечаянно изменить константу


                                        Так вот нечаяно — тебе ни один компилятор не даст изменить. И — да, именно на этапе компиляции.
                                        А если ты const_cast'ами направо и налево размахиваешь — ну так это ты сам себе злобный буратин.
                                        И какая программисту разница как именно внутри runtime реализована константа? Для тебя она — константа.
                                        Если конечно ты всё-таки не захочешь странного.

                                        А в хаскеле наверное указателей и X-cast'ов нет?

                                        Ну а про счётчик цикла — это просто какая-то более сильная религия чем даже запрет goto :)
                                        • 0
                                          Разницы-то оно конечно нет, но почему-то проблема которое десятилетие очень остро стоит. Разница наверно в том что в одном языке приходится постоянно костылями пользоваться а в другом нет.
                                          Конечно, лучше ошибок не делать быть здоровым и богатым. Но статистика вещь упрямая, почему-то люди упорно не хотят сочетать все эти факторы и регулярно гуляют по полям из грабель.
                                          • 0
                                            Проблема модификации констант?
                                            Мне кажется Вы надумываете лишнего.
                                            Я за 20 лет программирования ни разу с такой проблемой не сталкивался.
                                            Да и в коде эти места будут шиты белыми нитками: не зря же const_cast придуман.
                                        • 0
                                          Все преобразования типов в Haskell явные. И не константных величин нет.
                                          • 0
                                            А вот там выше приводили пример с n1 и n.
                                            Это что?
                                            • 0
                                              Формально говоря, именованные величины некоторого типа, относящего к классу типов Num (раз для них определен (+)). Но в речи все их называют переменными, хотя изменяться они не могут.
                                              • 0
                                                А что значит?
                                                let n=n+1
                                                • +1
                                                  Попытаться определить величину n, которая равна себе плюс один. Скорее всего окончится ошибкой runtime при попытке его использовать (если не определить хитрый тип, для которго это уравнение имеет решение и компилятор сможет его вывести). Но написать такое случайно маловероятно и эта ошибка легко найдется.
                                                  В других языках, таких как SML, OCaml, F# (а так же Racket, хоть он не из этой серии) различают конструкции let и let rec — первая создаст новую величину n, равную старой величине n+1, и с новой областью видимости. Вторая выдаст ошибку компиляции, поскольку не умеет решать такие уравнения.
                                                  • 0
                                                    Да-а… brainfuck прям какой-то…
                                                    • +1
                                                      Наоборот, все выглядит как на бумаге математически задачу описываешь.
                                                      • 0
                                                        Так математика ж brainfuck и есть :) Но в хорошем смысле этого слова
                      • 0
                        Берите любой большой проект на Haskell или Rust и смотрите, дефектов там не меньше, чем у других. Формальная верификация такого кода тоже может заметно уменьшить их количество.

                        Просто причина совсем не в математике, причина в сложности, которой «земляне» могут оперировать. И если атаковать одну и ту же проблему двумя принципиально разными методами или на двух совершенно разных уровнях для подстраховки, то при вероятности ошибки 0,01 в каждой строчке обоих методов мы все равно снижаем вероятность одновременного присутствия ошибок в обоих до 0.01*0,01, т.е. до 0.0001. В этом вся суть.
                        • 0
                          Интерсно сравнить.
                          На моем опыте в двух сравнимых проектах — модель суперскалярного процессора MIPS на Haskell и прочессора с архитектурой потока данных на C++ — дефектов в первом было меньше. Правда, мнение субективное, я в обоих проектах участвовал.
        • 0
          Давайте по пунктам.

          1. Способность логично и алгоритмически мыслить — не формализуется и не измеряется.
          2. Код хорошо читаемый кем конкретно? Если специалистом в той же области и того же уровня, то это одно, а если даже новичками или волонтерами — совсем другое. Слишком размыто.
          3. Неконкретно.
          4. А всезнанием и просветлением он обладать не должен? Хорошо, когда специалист хорошо знает хотя бы несколько популярных технологий и инструментов и имеет представление о еще полудесятке.
          5. Да что уж, пусть сразу знает топологию всех используемых чипов и детали процесса производства.
          6. Все программисты способны разрабатывать все. Вопрос во времени и эффективности.
          7. С базовыми принципами работы баз данных можно ознакомиться за три минуты в вики. Получить реальный опыт работы с БД в проектах с высокой нагрузкой или высокой сложностью — совсем другое дело.

          И дальше все примерно так же. Все это совершенно не важно, поскольку отражает лишь субъективное восприятие собственного опыта. А раз так, то зачем изобретать очередной велосипед на костылях — возьмите какой-нибудь типичный опросник для программистов типа Programmer skill matrix (их много разных уже придумали).

          Что особенно забавно, так это то, что в вашем видении «специалист высокого класса» не должен иметь представления о командной работе и документировании кода. Этим, дескать, должен заниматься лишь руководитель.
          • 0
            1. Тесты на логику и задачи на программирование
            2. Читаемый всеми, средним специалистом

            > «специалист высокого класса» не должен иметь представления о командной работе и документировании кода

            это всего-лишь группировка скилов по типам, это не значит что кто-то не должен знать
            • +1
              1. «Задача на программирование» звучит примерно так же странно как «задача на науку». Программирование охватывает огромное количество областей.

              2. «Средний специалист» — это тоже абстракция. В разных компаниях разное понятие «среднего». Вполне возможно, что того, кого вы считаете средним специалистом, кто-то будет считать высококлассным, а кто-то такого даже стажером не возьмет.
            • 0
              Пример из жизни: по тестам человек отлично все знает, но отсутствие реального опыта просто не дает ему решать целый класс задач.
  • +7
    Все причины можно уместить в одну: Коммерциализация. Даже полёт на луну это продажа идеи конкурирующей с другой.
    • 0
      И это хорошо. Деньги — отличный стимул. Остальные либо не работают либо кончаются войной.
      • +2
        А деньги и работают, и войной не кончаются?
  • 0
    Мне кажется, дело еще и в том. что вместо одного «железячника» для хардварного решения части проблем проще нанять 10 «индусов» для ее софтварного решения.
    Например, я столкнулся с проблемой — нужен был счетчик импульсов на 12 разрядов. Большая часть микросхем мелкой логики, на которой его можно построить, уже снята с производства. И на меня смотрели как на идиота — мол, делай на МК и все. Один корпус вместо двух десятков и прочее. Но мне нужна была абсолютная устойчивость (помехи, МК может виснуть, железное решение, стоявшее там до этого не висло при грамотной экранировке совсем и никогда), плюс еще некоторые хитрые параметры. Почему «железячные» решения исчезают в угоду софту — мне непонятно. Но это меня не радует.
    • +3
      Универсальность видимо, проще делать одну железку на все случаи жизни, чем сотню разных и это не проблема если схема этой универсальной железки математически надёжна.
      • +1
        Проще для производителя — может быть, проще для пользователя — не уверен. Специализированное устройство всегда эффективнее и удобнее «комбайна». построенного на компромиссах.
        • +2
          Да в какой-то момент эффективность универсального решения может стать столь высокой, что практической разницы со специализированным не будет.
          Ну и пользователю проще изучить одно решение чем каждый раз доки читать. (если что минус не мой)
    • +4
      Счётчик на МК может быть менее чувствителен к помехам, поскольку у него нет множества достаточно длинных проводников, соединяющих логические элементы, на которые может быть наведена помеха. И если частота импульсов низкая — его можно снабдить множеством программных средств самоконтроля, при помощи которых можно добиться высокой вероятности его правильной работы даже в случае, если в МК произойдёт сбой.
      • +1
        А в дубовой логике оно просто работает десятилетиями без средств самоконтроля и иных костылей.
      • 0
        Максимум, что грозит устройству на логике, — перескок через несколько «тиков» счёта или сброс в начальное состояние и новый отсчёт с нуля. Иными словами, помеха может изменить текущее состояние устройства, но не может нарушить его нормального функционирования.
        При этом МК может творить всякие чудеса от перескока на совершенно неожиданную ветку программы вплоть до полного зависания, выдернуть из которого его может только отключение питания.

        • 0
          Если использовать brown-out детектор и watchdog-таймер — МК как правило тоже не творит чудеса, а сбрасывается, и даже не теряет при этом данные и может продолжить счёт — валидность данных можно проверить по их копии. А сброс в начальное состояние, факт которого даже не фиксируется — это не нормальное функционирование.
          • +2
            Ключевое слово — «как правило».
            К сожалению, в реальности и с включенным watchdog таймером МК порой намертво зависает. Реже, чем без него, но всё-таки зависает.
            • +3
              Точно так же может зависнуть и аппаратный счетчик — триггерный эффект по входу из-за наводки и вход не работает до передёргивания питания(в лучшем случае).
              Возьмём к примеру классический счётчик джонсона(561ИЕ8), который может иметь запрещённые(невалидные) состояния, наведённые помехами и только специально спроектированная схема позволяет счётчику выйти в одно из рабочих состояний за конечное количество тактов.
              Если взять более сложные схемы на логике(Привет ПЛИС) то там так же достаточно много «программных заморочек» где что-то может пойти не так. Даже обычный триггер можно манипуляциями входных сигналов ввести в невалидное состояние. Попробуйте узнать для чего вообще придумали двойные(с двойной защелкой) D-триггеры. И всё это является примером того как в программах преодолевают сбои, только на аппаратном уровне. И даже двойная защёлка не убирает аппаратную проблему простого триггера а только лишь уменьшает вероятность её возникновения.
              А ещё есть race condition…
    • 0
      Сейчас уникальную аппаратную логику наверное на ПЛИСах делают.
    • 0
      ПЛИС вам чем не угодили? Рассыпуха уже и правда прошлый век под вашу задачу хорошо бы подошла любая ПЛИС.
      • +1
        Пожалуй, у большинства ПЛИС больше проблем будет даже чем с МК. Уж больно они чувствительны к нагрузкам на выходе, наводкам на воде вызывающих порой тиристорный эффект и чистоте питающего напряжения. А ещё, что более ужасно, в эквивалентных схемах(рассыпуха vs ПЛИС) в ПЛИС задействовано больше элементов в цепочке снижающих надёжность всей конструкции.
        • 0
          Еще одна проблема — «время жизни» чипа. То, что выходило 5-7лет назад, давно снято с производства С ПЛИС в этом отношении проще МК (прошивку можно залить в разные плис, чуть подправив), но плату все равно придется переделывать.
    • 0
      Жесткая логика до сих пор производится, никто ее не снимал с производства. Накрайняк на PLM изобразить можно.
  • +3
    Земляне делают глючный софт, потому, что сами глючные, довольствуются глючным софтом, применяют при производстве глючные подходы, наказывает кого попало, а не того кто наделал глюков и важно им совсем не безглючность а что бы было быстро сделано, свиду работало и клиент быстрее заплатил.
  • +3
    Желязны не писал рассказ «Когда расцветают бомбы».

    Это известная литературная мистификация.
  • +19
    Господа, опомнитесь! Кода это были те светлые «не коммерциализированные» времена, когда ошибок в программах не было? Вы случайно планетой не ошиблись?
    В прикладных программах всегда были баги. В картриджах для игровых приставок (ПЗУ, новую версию не накатишь) были баги, в операционных системах со времён их появления были баги, в микрокодах процессоров были, да даже в топологии процессоров были баги.
    На военных спутниках и самолётах были баги, и это несмотря на смехотворный по нынешним меркам объём кода, простой как топор процессор и 10 колец оцепления со всеми существующими способами их устранения.

    Не было никогда безглючного софта и не будет никогда. Это фундаментально невозможно.

    А тем, кому не нравится «коммерциализация», можно предложить альтернативу — вы будете покупать железо, которое стоит как ваша квартира? Игры не за 4 тысячи, а за 40? Пустой интернет, потому что все профессора информационных технологий в стране завалены заказами на год вперёд. Всеми 10-ю заказами? Прикладной софт, не обновляющийся десятилетиями по этой-же причине? А то, что его ещё и меньше будет на пару порядков?
    И всё это ради того, чтобы частота возникновения ошибок сократилась с «1 раз в неделю» до «1 раз в год».

    На сам-то деле всё проще. Программа (и железо) нужна чтобы решать какую-то задачу, у неё нет самоцели быть правильной. Глюков, багов и недоработок в ней будет ровно столько, сколько экономически обоснованно. Всегда есть предел, после которого затраты на дальнейшее улучшение начинают превосходить полезный эффект от этих изменений.
    • 0
      Увы, потребности рынка в специалистах чудовищны, а специалистов мало.
      • 0
        В данном случае речь о защите от техногенных катастроф связанных с ошибками в ПО
        • 0
          Технологически безопасный софт всё-таки живёт по другим правилам нежели «офисный».
          • 0
            я об этом писал и даже приводил ссылку
    • –3
      Вы не правы. Безглючный софт фундаментально возможен. Я могу это доказать, к примеру вывод какого-нибудь «hello world» — вполне себе софт, и там не будет багов, негде просто. Если сильно заморочиться идеей безглючности можно этот «hello world» на ассемблере написать, дабы избавиться от лишних прослоек в виде компиляторов/интерпретаторов.
      Для написания более сложного безглючного софта существуют специальные методики(см. formal verification).
      Другое дело, что методики не защищают от архитектурных или логических ошибок.

      С чем я могу полностью согласиться, так это с тем, что безглючный софт комерчески совершенно не целесообразен.
      • +5
        Если сильно заморочиться идеей безглючности можно этот «hello world» на ассемблере написать, дабы избавиться от лишних прослоек в виде компиляторов/интерпретаторов.

        Для багов остаётся ОС со всем букетом драйверов, прошивки железа, само железо.
        • –3
          Возмите микроконтроллер который вам будет азбукой морзе лампочкой мигать.
          • +1
            Ну вот и пришли к тому, что или микроконтроллёр, бесполезно мигающий лампочками, или ПК с 4 ядрами, гигабайтами и SSD, и запущенным на нём браузером, падающим раз в неделю.
          • +3
            Не, мигающий микроконтроллер это сильно сложная вещь. У вас будет на «поиграть» вместо современного компьютера 3-х знаковый калькулятор.
            Что убирает сразу много классов задач(те же игры становятся очень дорогими) и как результат полностью убирает экономический смысл улучшения архитектуры(и фраза деректора IBM про рынок компьютеров в размере 5 штук на планету становится правдой).
            Кому нужен микроконтроллер с лампочками, если верификация его ПО потребует суперкомпьютера(ВЕРИФИЦИРОВАННОГО с верифицированным ПО), которого ни у кого нет.
          • +1
            Возмите микроконтроллер который вам будет азбукой морзе лампочкой мигать.

            … который глюканёт при сбое питания. Попытаетесь предотвратить это событие — наткнётесь на баг аппаратной части этого контроллера (которых немеряно, почитайте даташиты в конце). Закажете партию МК без этих багов — получите мигалку космической приёмки по цене топового смартфона.
      • 0
        Максимум, что можно решить математически — это валидность программы с точки зрения языка + наличие «защиты от дурака». Но нет ни единого способа определить, что работающая программа работает правильно, т.к. она и есть наиболее полное формальное описание, как должно быть правильно.
        • +1
          Ну если вы утверждаете что нет такого способа, то конечно мне придётся удалить статью и забыть словосочетание «формальная верификация»
          • 0
            «формальная верификация» — это не какой-то механизм, который можно автоматизировать для общего случая, как например статический анализ. Это индивидуальная работа по каждому конкретному случаю.

            Кроме того, то что я не просто так написал «программа и есть наиболее полное формальное описание, как должно быть правильно». Если у вас верификация более проработана, чем программный код, то она фактически становится первичным исходником программы, по которому строится всё остальное. И мы снова упираемся в то, с чего начали, как проверить, что мы при верификации учли все возможные ошибки, если её результат — это самое исчерпывающее описание программы?
            • 0
              вы удивитесь, но я об этом писал в статье, и дополнительно отвечал тут
              • 0
                Да я собственно и не спорю ни с вами ни со статьёй.
                Просто вы написали «есть такая метода чтобы свести ошибки почти к нулю» и началось: «а вот как хорошо раньше было», «а ведь можно же всё делать хорошо», «какую страну индустрию просрали», «это всё коммерсанты виноваты».
                А то, что эта метода имеет имеет астрономическую стоимость, да к тому же тоже не без изъяна, и поэтому в «повседневной работе» не особо применима, все как-то из виду упускают.
        • 0
          А как насчёт?
          «стиль программирования под названием формальное подтверждение. В отличие от обычного кода, написанного неформально и оцениваемого обычно только по его работоспособности, формально подтверждённое ПО выглядит, как математическое доказательство: каждое утверждение логически вытекает из предыдущего. Всю программу можно проверить с той же уверенностью, что и математическую теорему.»

          https://geektimes.ru/post/282234/
        • +4
          Можно, один из них — теория типов.

          У вас сейчас статически типизированные программы типизированы не полностью. Т.е. у вас в наличии функции типа «принимает массив с элементами типа T и число, возвращает элемент типа T или создаёт исключение».

          А в более мощных системах типизации (где есть зависимые типы) можно иметь функции типа «принимает массив длины n с элементами типа T, число m, которое больше либо равно нуля, строго меньше n, возвращает элемент типа T».

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

          И так можно описывать абсолютно что угодно, включая то, как должны обрабатываться внешние события, хотя никто не верит.
          • 0
            и как интересно статическая типизация должна справиться с этим, если этот массив создается в рантайме? Вы, конечно, можете возразить что сам тип массива должен включать ограничение на длину, но тогда весь код будет засран уникальными типами. Здесь массив не больше 4, там не больше 6. В третьем месте от 3 до 8 и т.д. Самое близкое к реальной жизни что я видел, это «контракты», когда на входе в метод параметры проверяются на ограничения (к примеру как у вас). Видел даже несколько библиотек для java, можно посмотреть здесь в разделе Languages with third-party support https://en.wikipedia.org/wiki/Design_by_contract
            По личному опыту самое простое это использование prerequest в начале метода (к примеру из guava). Но в любом случае это не compile-time validation.
            • 0
              прошу прощения, Precondition.
            • 0
              Не, у нас нет уникальных типов, есть вполне общий Массив n элементов типа T.

              И никто не мешает использовать эту n в рантайме.

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

              Но, например, если мы просто хотим обойти весь массив, то если мы устроим цикл от 0 до n — нам не потребуется ничего проверять, т.к. будет тривиально получить пруф того, что индекс будет меньше n, ибо нам его генерит цикл и никуда не меняет больше.

              Буду дома, может накидаю какой пример кода, как именно оно будет проверяться.
            • 0
              Вопрос в том насколько у вас мощная система типов. Например на scala:
              class MyArray[N <: Nat, T] private (private val arr: Array[T]) {
                def get[I <: Nat: ToInt](i: I)(implicit ev: I LT N) = arr(Nat.toInt[I])
              }
              object MyArray {
                def apply[N <: Nat: ToInt, T: ClassTag](n: N)(f: Int => T) =
                  new MyArray[N, T](Array.tabulate(Nat.toInt[N])(f))
              }
              
              val ma = MyArray(Nat(5)){ i => s"element $i" }
              
              ma.get(Nat(0)) 
              // res1: String = "element 0"
              ma.get(Nat(1)) 
              // res2: String = "element 1"
              ma.get(Nat(4)) 
              // res3: String = "element 4"
              ma.get(Nat(5)) 
              // cmd10.sc:1: could not find implicit value for parameter ev: shapeless.ops.nat.LT[...]
              // val res10 = ma.get(Nat(5))
              //                   ^
              // Compilation Failed
              

              Scala тут, кстати, не уникальна.
            • 0
              Это умеют проверять так называемые «зависимые типы». Но ими пользоваться обычно тяжело.
              К счастью, это не на столько частая ошибка, если с массивами в основном работать с помощью инетретором и отлаженных функций высжего порядка (map, fold и тп).
      • 0
        О, давайте! Спустимся в процессор и будем физически доказывать его непоколебимость? Свободу от наводок палящего излучения и физической невозможностью «забыть» какой либо бит? Давайте! Спустимся в физику и будем доказывать её непоколебимость? Докажем работоспособность p-n переходов в любых условиях и приручим заведомо случайную, почему нет? Давайте! А сверху ещё останутся виртуальные машины, операционные системы реального времени и различные архитектуры процессоров, от велосипедов на ферромагинитах до 64-битных ARM Cortex A72. А ещё можно продолжить быдлокодить где быдлокодили и не лезть к серьёзным людям, занимающимся настоящей работой, навроде проектирования радиоаппаратуры и интегральных схем. Потому что душа без тела никому не нужна, а вот тело с кривой душой вполне работоспособно. Всегда есть риски, нельзя взять и уйти от них.

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

        Ко всему прочему, мы до сих пор не могём разрешить нелинейных дифференциальных уравнений в системе с парой десятков неизвестных (читай, энергетически оптимальный запуск ракеты), что уж говорить про тензорную и топологическую ересь.
        • 0
          На первый вопрос ответил тут https://geektimes.ru/post/283804/?reply_to=9760964#comment_9761208

          А то что Гёдель доказал вам стоит почитать ещё раз, математика не может ошибаться если она непротиворечива, но при этом может быть неполна (т.е. какие-то истинные утверждения могут быть невыводимы, но это цена за точность), а вот если полна, то может ошибаться, но такой вариант видимо на практике бесполезен.
          • 0
            При чём тут кремний? Я говорю про фундаментальную невозможность сделать наверняка, вы говорите кремний самый надёжный. Вы говорите Гёдель доказал, что математика не может ошибаться если, я хочу заметить, что при этом в ней будут нерешённые задачи, априори. Да и банальные ошибки в доказательствах возможны, в комбинаторике постоянно опровергают доказательства.
      • +1
        Внезапно, правильный hello world на сях не так тривиален, как может показаться :)
        удивляемся, читая это http://erdani.com/tdpl/2010-12-08-ACCU.pdf с 11 страницы
      • 0
        Даже тут можно незаметно для себя вывести «hell world», что радикально меняет смысл…
    • +1
      Вот хочу чуть-чуть процитировать Бориса Чертока, он работал с атомщиками, когда делали первую «атомную» ракету Р-5, и немного писал про то, как собирали атомные бомбы.

      Нам предстояло разработать технологию совместных испытаний двух «изделий в целом» после их стыковки и весь многоступенчатый технологический план работ на стартовой позиции. Эту работу Королёв поручил молодому заместителю Воскресенского Евгению Шабарову. Почему не самому Воскресенскому? Здесь в который раз я убедился в умении Королёва выбирать людей для соответствующей задачи.

      Воскресенский был испытатель высшего класса, одаренный необычайной интуицией. Кто-то метко его охарактеризовал: если бы он был лётчиком, то рисковал бы, как Чкалов. В отношениях с атомщиками партизанские действия были абсолютно недопустимы. Кроме существа дела, требовалась и его чёткая, последовательная формализация.

      Что будет, если при подготовке ракета с атомной бомбой свалится у старта по причине, аналогичной упомянутому выше разгильдяйству с незакрытым баком перманганата натрия? Методика работы атомщиков предусматривала тройной контроль всех операций по сборке и испытаниям. Руководитель сборки или испытаний держит инструкцию и слушает, как испытатель громко читает содержание операции, например: «Отвернуть пять болтов, крепящие крышку такую-то». Исполнитель отворачивает. Третий участник работ докладывает: «Пять таких-то болтов отвернуты». Контролёр — представитель военной приемки — докладывает, что выполнение операции принял. Об этом делается роспись в соответствующем документе. Только после этого вся компания может переходить к следующей операции. Работа идет медленно, скрупулёзно, с обязательной громкой читкой, обязательным громким докладом об исполнении и распиской в особом технологическом журнале.

      У нас таких строгих формальностей не было. Когда Шабаров обо всей этой методике рассказал Королёву, тот решил, что там, где мы будем работать вместе, надо «им показать, что мы не хуже». Ну, а что касалось нашей собственной деятельности, то для ракеты Р-5М необходимо было пересмотреть все инструкции по подготовке на технической и стартовой позициях и тоже ввести тройной контроль: основной исполнитель — воинская часть (офицер или солдат), контролирует офицер — специалист соответствующего управления полигона и обязательно представитель промышленности.


      Так что и раньше в принципе можно было резко снизить брак и глюки в критически важных местах, но видно же, какое это мучение, как это долго и экономически невыгодно. Нужна некая золотая середина.
      Другое дело — что если, как worldmind пишет, удастся сделать технические средства для устранения багов в коде и железе математическим путём и, разработав эту систему 1 раз, дальше можно будет использовать без затрат — это было бы неплохо.
  • 0
    Потому что земляне сами глючные, у кого-то криворукость, у кого-то дальнозоркость, кто-то быстро пишет код, но мало проверяет… Эволюция — выживают сильнейшие. И программы такие же выживают сильнешие, но глючат все…
    Глючность это преимущество.
    • 0
      Эволюция — выживают сильнейшие.
      Известное заблуждение: на самом деле суть в размножении. Биология поведения человека. Лекция #2. Эволюция поведения, I [Роберт Сапольски, 2010. Стэнфорд].
      • 0
        «Эволюция — выживают сильнейшие», это крылатое выражение в данном контексте к тому, что останутся наиболее стабильные и полезные программы. А в биологии это значит, выживают (остаются) сильнейшие (наиболее полезные) признаки.
        • +2

          Вовсе нет. В биологии это означает "выживают выжившие", то есть приспособленные. Сильнейшие признаки? Саблезубые тигры имели большие проблемы с позвоночником, и так по всему комбинату. А мыши пережили динозавров. В чем сила?

    • 0
      Глючность нужна при эволюции, а те программы о которых речь не эволюционируют (не размножаются и не подлежат отбору)
      • 0
        Глючность — мутации. Суть в том, что неизвестно какое качество полезно, пусть появляются. Главный вопрос — «почему земляне делают глючный софт и железо», ответ — потому что сами такие.
        Лучше написать глючную, но полезную программу, чем написать хорошую бесполезную. В принципе и бизнес так думает.
        Было бы кому-то нужно написали бы идеальные программы. В математике (!), о которой идет речь строгих доказательств до 20 века не было. Эйлер суммировал расходящиеся ряды, Рамануджан большинство формул выводил методом приближений и иногда даже не доказывал, а уважаемый Ферма по всем решениям оставлял заметки на полях, с одной, правда, задачей плохо получилось.
        Не пытаюсь никого переспорить, математика не формализировалась, пока это не стало нужно. Сейчас программы работают относительно стабильно, а ошибки быстро исправляются, зачем формальные доказательства?
        • 0
          вы похоже не читали статью, я не про бизнес программы веду речь
        • 0
          В математике (!), о которой идет речь строгих доказательств до 20 века не было.

          А как же Евклид?
  • +9
    кто уверен что вирус не начнёт ядерную войну?

    Ядерная война,
    Ядерная война,
    Кто мне расскажет, кто подскажет,
    Скоро ли она?

    • –1
      Станислав Евграфович Петров вроде говорил, что вероятность ошибки или попадания в руки террористов вопрос времени. Эксперта по этому вопросу лучше него вряд ли возможно найти.
    • +2
      Ядерная война определенно переоценена. Мощность всего ядерного арсенала сравнима с всего одним пусть сильным, но даже не рекордным супервулканом. Ну, а заражение радиацией конечно неприятно но не смертельно.
      • 0

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

        • +1
          Брешут.
        • 0
          Ну, во-первых раньше их было больше — не сильно но в несколько раз, правда это ничего качественно не изменит. Думаю преувеличивают для красного словца… разве что таки заражение радиацией имеют ввиду, хотя в инете говорится что за ~80 лет ядерной эры человечество уже взорвало около пол-гигатонны ядерного материала (в основном в тестах) (примерно 15% из этого — царь-бомба) и это почти не заметно, то вряд ли то что осталось даст сильный эффект. Конечно если использовать их по-назначению — т.е. взрывать в больших мегаполисах, то цивилизация сильно пострадает, может даже скатится до уровня мэдмэкса/фоллаута (на земле хватает мест где это само собой случается, без какой-либо ядерной войны), но земле вряд ли что будет.

          Собственно, уничтожить землю буквально, как в «лекксе», по моему невозможно в принципе — грав. энергия связи слишком большая, первая космическая скорость соответствует температуре в порядка сотни тысяч градусов. Т.е. ее сначала нужно расплавить и испарить, а потому уже она начнет убывать в космос.
      • –1
        Действительно, переоценка такая сильная. Ничтожная переоценка, вон я смотрю в Чернобыле, Фукусиме прекрасно живут люди, выращивают пищу себе в почве, а не собирают её в мешки, разводят скот, а не забивают тысячи голов скота. И это ничтожные Уран-238 и Торий-232, при ядерном взрыве загрязнение начинается Плутонием-239 и Ураном-235. Загуглите их активность, тысячекратно выше. Смертельную дозу в 1 зиверт можно набрать за минуты.
        • +1
          На месте взрыва хиросимской бомбы действительно живут люди, и не парятся особо.
          • 0
            Ну так бомба было неэффективной.
            • +1
              Скорее наоборот, современные бомбы меньше загрязняют поверхность, так как захватчику нужно земли, пускай и через несколько лет, а не радиоактивная пустыня на ближайшие 40000 лет.
            • +1
              Вроде как наоборот, для ядерных бомб чем эффективней — тем меньше фоллаута на единицу мегатонн. Ведь их главная цель — поджечь и разрушить инфраструктуру.
        • +1
          при ядерном взрыве загрязнение начинается Плутонием-239 и Ураном-235. Загуглите их активность, тысячекратно выше

          Бред. При взрыве атомного боеприпаса (хоть уранового, хоть плутониевого) загрязнение обуславливается осколками деления исходного материала боеприпаса.
          Сам по себе уран-235 практически не радиоактивен, его период полураспада составляет порядка 10^8 лет. Это красноречиво говорит о его активности. У плутония-293 период полураспада 24000 лет, активность повыше, конечно. Давайте попробуем прикинуть величину загрязнения, если предположить, что плутониевый заряд не взорвался, а просто равномерно распылился по территории вследствие взрыва обычного ВВ (аналог «грязной бомбы»). Считаем:
          Дано: активность одного грамма плутония-239 — 2,3ГБк, масса боезаряда порядка 50 кг, распыление происходит на круг диаметром 5 км.
          Пересчитаю активность из беккерелей в кюри, получу активность грамма плутония 62мКu, активность всего боезаряда — 3108Кu. Площадь круга радиусом 5 км составит 78,5 кв.км. На каждый квадратный метр при этом придется активность порядка 40 мкКu, или примерно 1,5МБк. Это много. Но зиверт за минуту не набрать.

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

            Ну если посчитать и другие радионуклиды в центре взрыва, то можно и поспорить. В любом случае я хотел показать, что при ядерном взрыве заражение гораздо более серьёзное, чем при аварии на АЭС.
            • +1
              У вас не получилось это показать.
            • 0
              Давайте попробуем посчитать.
              Дано — реактор ВВЭР-1000. Масса топлива в одном ТВЭл — 1,565 кг. В тепловыделяющей сборке (ТВС) 312 ТВЭл, в активной зоне 163 ТВС. Итого общая масса топлива в активной зоне составит 79589 кг. Так как обогащение топлива у ВВЭР-1000 составляет от 3,3 до 4,4 процента (возьмем в среднем за 4 процента), то масса чистого U-235 составит 3183 кг. Предположим, что выгорание составило 50%, то есть, распалась половина массы U-235 — все атомы в 1590 кг урана распались на осколки (крайне радиоактивные, как я уже говорил).
              Теперь сравниваем это массу радиоактивных веществ с массой радиоактивных веществ, образовавшихся при делении всех атомов U-235 в 100 кг атомного боеприпаса.
              Итак, при тепловом (неатомном) взрыве на АЭС и произошедшем вследствие этого распределении топлива по территории загрязнение в 15 раз превысит аналогичное загрязнение от взрыва атомного боеприпаса.
              Конечно, это некорректное сравнение в плане того. что мы не учитываем другие поражающие факторы атомного взрыва — ЭМИ, нейтронный поток, световое излучение, ударная волна. Плюс, естественно, при атомном взрыве радиоактивные вещества будут разбросаны на бОльшее расстояние, чем при тепловом взрыве на АЭС. По совокупности поражающих факторов ущерб от атомного взрыва, скорее всего, будет превосходить ущерб от теплового взрыва на АЭС.
              Но если говорить только о загрязнении, то в последнем случае загрязнение будет значительно выше (чисто по массе РВ — в 15 раз), плюс распределится это загрязнение на меньшую площадь, а значит, удельное загрязнение на единицу площади будет еще больше.
            • 0
              И это, кстати, мы посчитали только по топливу, без учета массы конструкций активной зоны, которые вследствие постоянного облучения нейтронами приобрели наведенную радиоактивность, а значит, тоже будут давать вклад в загрязнение.
              • 0
                Наведённая активность быстро сходит на нет. Это если в структуру материала внедрились атома радиоактивного вещества — только тогда будет проблема. Но это по большей части лишь поверхностное загрязнение.
                • +1
                  Вы не правы. Наведенная активность главным образом обусловлена облучением материала потоком нейтронов. Атом стабильного изотопа может захватить нейтрон и превратиться в нестабильный (т.е., радиоактивный) изотоп. А как быстро наведенная активность «сойдет на нет» — будет зависеть только от вида полученных изотопов, в зависимости от их периода полураспада.

                  Погуглите, что такое «наведенная активность», если не верите мне.
                  • 0
                    Только вот если материал не урановый лом, долгоживущих изотопов не выходит. Основная проблема загрязнения материалов — это поверхностная активность, хуже конечно когда железка 30 лет работала в реакторе — тогда да, будет долго «остывать» ещё и за счёт диффузии изотопов топлива в материал.
                    • +1
                      Вы спорите ради спора, не утруждая себя поиском собственных аргументов и проверкой аргументов оппонента?
                      Вот нашел с ходу:
                      А это цитата оттуда:
                      Например, нежелательно содержание в таких сплавах никеля, молибдена, ниобия, серебра, висмута: они при облучении нейтронами дают изотопы с длительным временем жизни, например 59Ni (T½ = 100 тыс. лет), 94Nb (T½=20 тыс. лет), 91Nb (T½=680 лет), 93Mo (T½=4 тыс. лет). В термоядерных реакторах нежелательным материалом является также алюминий, в котором под действием быстрых нейтронов нарабатывается долгоживущий изотоп 26Al (T½=700 тыс. лет). В то же время такие материалы, как ванадий, хром, марганец, титан, вольфрам не создают изотопов с длительным временем жизни, поэтому после выдержки в течение нескольких десятков лет активность их падает до уровня, допускающего работу с ними персонала без специальной защиты. Например, сплав 79 % ванадия и 21 % титана, облучённый нейтронами спектра термоядерного реактора DEMO с флюенсом 2·1023 см−2, за 30 лет выдержки уменьшает активность до безопасного уровня (25 мкЗв/ч), а малоактивируемая сталь марки Fe12Cr20MnW только за 100 лет. Однако даже небольшая примесь никеля, ниобия или молибдена может увеличить это время до десятков тысяч лет.

                      Как видно, могут образовываться всякие изотопы и сравнительно короткоживущие, и долгоживущие. Но время снижения активности до безопасного уровня даже у короткоживущих — это 10-20-30 лет. Тоже немало на самом деле.
  • +2
    Есть такой метод/подход к написанию программ, называется formal verification(формальное доказательство) и вытекающее из него «доказательное программирование». Так что идея ваша совсем не нова, она была довольно популярна в академ кругах в 70-х, 80-х годах.
    Идея не пережила коммерциализацию, в связи с крайне высоким уровнем сложности реализации для сколько-то сложных программ. На данный момент впрочем, в связи с ростом связности систем, интерес к концепции по немногу возрождается.
    • 0
      Именно об этом подходе моя статья
      • +1
        А вот можно «на пальцах», так сказать, рассказать как технически может выглядеть построение программного обеспечения системы, например, управления поездами на станции?
        Просто статьи про функционально безопасное ПО зачастую очень общи, содержат пространные рассуждения, много воды. И эта статья не исключение.
        А вот если приземлённо, без теоретизирования: объясните программистам пишущим софт для управления железнодорожной станцией — как они должны его писать?
        Чтобы рассуждения не были опять-таки отвлеченными, пусть структура системы будет такой:
        1. Т.н. напольное оборудование (стрелки, сигналы, рельсовые цепи, ну и всякое по-мелочи).
        2. Шкаф управления напольным оборудованием обеспечивает безопасную увязку с п.1. Функционально безопасную. Т.е. объекты будут изменять состояние только по командам и никак не самопроизвольно, сигнализация от объектов будет поступать корректная, однозначно соответствующая их реальному состоянию. Это, вообще говоря, тоже не тривиальная задача.
        3. Центральный Вычислительный Комплекс (ЦВК).
        4. АРМ пользователя. Собственно он не обязан быть безопасным. Вся безопасность заключается в ЦВК.

        ЦВК это, к примеру, трёхканальная система, работающая по мажоритарному принципу (2-из-3). Если один канал начинает выдавать данные, не совпадающие с остальными двумя — он отключается и система начинает «хромать» по принципу 2-из-2: ЦВК управляет только пока выходные данные обоих оставшихся комплектов совпадают. Возможно с урезанием функционала.
        Если же начинают расходиться данные оставшихся комплектов — система переходит в защитное состояние до вмешательства обслуживающего персонала.

        Чисто алгоритмически, ЦВК выполняет увязку стрелок, сигналов и рельсовых цепей так, чтобы не допустить враждебностей и опасных воздействий на подвижной состав (перевод стрелки под составом, некорректное перекрытие сигнала перед поездом).
        Ну и, понятно, нужно обеспечить пропуск поездов по станции с требуемой интенсивностью.

        Как к данной задаче применить упомянутый Вами метод создания ПО?
        • 0
          Писать-то можно также, а вот проверять по другому — математически доказывая, что программа делает, то, что описано в требованиях, я приводил ссылку на доказанное микроядро — у них вроде опубликована научная работа о том как они это делали.
          Без теоретизирования математическую теорию никак не объяснить, но тут в комментах говорят о знакомстве с теми, кто занимается формальной верификации, можете попробовать напросится на лекцию.
          • 0
            Писать-то можно также, а вот проверять по другому

            Как же «также»?
            • 0
              В соответствии с методологиями применяемыми в таких сферах, обычно в таких компаниях процесс налажен и/или есть внешние требования от сертифицирующей организации, у меня вопрос вызывает ассоциации с Pmbok и т.п.
              • 0
                Ладно.
                И как доказать, что в программе нет зависимости состояния сигнала в одной горловине от положения стрелки — в другой? Кроме нормативного конечно.
                Полным перебором всех комбинаций всех значений всех сигналов и переменных со всеми временнЫми выдержками? (время — это тоже параметр)
                • 0
                  Изучить теорию доказательства программ и доказать. Вроде даже есть общедоступные онлайн курсы.
                  • +2
                    Я не пойму, Вы распинаетесь с этой идеей уже второй день и не хотите на предложенном примере проиллюстрировать её преимущества или хотя бы работоспособность?
                    • 0
                      Я же написал, что не специалист в этой сфере, о преимуществах и работоспособности я привёл ссылки, в дополнение могу ещё эту добавить.
                • +1
                  Почитайте вводные статьи по TLA+/TLC/TLAPS, как раз из вашей области. Вот пример на TLA+, для проверки подобного отсутствия зависимостей, правда для снэпшотов.
  • 0
    Современный персональный компьютер (ПК) — это всего лишь баловство, которое может помочь человеку самовыражаться. Через это самовыражение и происходит развитие, как человека, так и ПК. Человек балуется с ПК, а баги на ПК балуются с человеком, все тут сходится.
    Другое дело, если говорить о микропрограммах для жизненно важного оборудования, вот там да, стоимость бага сильно велика и конечно этому стоило бы уделять побольше внимания, возможно даже и на мировом уровне, вот только, что делать с «загребущими руками»? Если начинать вливать в эту отрасли большие деньги на зарплату, то сразу найдутся люди, которые просто будут нахлебниками и средний интеллект в такой команде не увеличится. Да, через пару тройку лет возможно и получится отсеять некоторых недобросовестных людей, но за это время добросовестные задолбутся получать по шапке за тех, кто криво делает. Наказания спросите вы? А что стоит наказания одного раздолбая, если выпущеный серийный аппарат МРТ, например, поджарит пару десятков человек?
    Ну дальше я не буду развивать эту тему, наверно стало немного понятно, что хорошее оборудование с малой вероятностью появления багов стоит очень дорого и не из-за того, что там работают дорогостоящие сотрудники и загребают деньги лопатой, а из-за того, что весь этот процесс очень и очень сложно организовать из-за человеческой натуры.
    Ровно из-за этого на наше с вами баловство с ПК ни кто не будет писать софт без багов.
    • +3
      если выпущеный серийный аппарат МРТ, например, поджарит пару десятков человек

      Серийно выпускаемые автомобили убивают около 3500 человек в мире каждый день. Многим это не нравится, но от автомобилей никто избавляться не спешит.
      • 0
        Я и не говорил, что от них надо избавляться. Более того, автомобили — поповозки — это в большинстве случаев тоже баловство и покупая себе автомобиль, человек берёт на себя ответственность в том числе и за его баги, Если они конечно не сильно явные и их можно интерпретировать, как особенность.
        • 0
          Я к тому, что смерть двадцати человек — это, конечно, не слишком хорошо, но люди умирают все время и потому важен баланс. Если из-за ожидания нового медицинского устройства погибнут 200 или 2000 человек, то риск, как мне кажется, оправдан. Я лишь хотел бы быть информированным о подобных рисках.
    • 0
      Никуда вливать ничего не нужно, нужно чтобы аппарат МРТ не проходил сертификацию, не допускался к эксплуатации если его прошивка не верифицирована.
      • +1
        Вот это будет очень большой проблемой в развитии любой отрасли. Если так сделать, то возможно останется одна фирма, которая сможет пройти сертификацию верифицировав весь свой код. Но стоимость будет заоблачной, Позволить себе это смогут только отдельные клиники, стоимость лечения в которых будет тоже очень высокой. Большенство людей останется без диагностики.

        Эту проблему надо решать по другому. А вот небольшой наброс на вентилятор: представь теперь, что писать код для него будет тот человек, которому этот аппарат необходим, какова вероятность того, что он халатно отнесётся к написанию программы?
        • 0
          Заоблачной стоимость будет только если каждый производитель каждый раз будет заново писать и верифицировать весь свой код, а если будут использованы ранее верифицированные открытые компоненты, то стоимость вырастет не сильно.

          А неважно насколько халатно человек отнесётся, человек при всём своём желании не может быть безошибочным, одни когнитивные искажения чего стоят, а есть куча других факторов (не доспал, простыл, отвлекли, не сообразил, забыл...) из-за которых даже самый ответственный человек может ошибиться.
          Человек не надёжное звено в любом случае, каким бы он ни был.
          • 0
            И вот тут мы подошли к самой главной теме, которая не раскрыта в этой статье «Стоимость и временные затраты на написание верифицированного кода»
            • 0
              отсюда: «Для проведения теста было взято микроядро Secure Embedded L4 (seL4), содержащее 8700 строк кода базирующегося на open source проекте OKL4…
              Работой по формулировке алгоритма математического доказательства в течение четырех лет занималась команда из 12 исследователей NICTA, аспирантов и техников. Они успешно проверили более 10 тыс. промежуточных теорем, изучив более чем 200 тыс. строк кода. Итоговый анализ выполняется с помощью интерактивной программы Isabelle, и на сегодняшний день является самой объемной автоматизированной проверкой выполнения условий теорем.
              Наряду с доказательством соответствия программного кода выполняемым функциям, тестирование показало, что seL4 не подвержен большинству известных хакерских атак. Например, атака «переполнение буфера», позволяющая внедрить злонамеренный код и захватить управление работой ядром, не даст результата.»

              Примерно миллион долларов и человечество получило микроядро беспрецедентной надёжности, доступное всем по свободной лицензии.
              • 0
                И 4 года на проверку, заметь не написание, а только на проверку. Плюс мне кажется, что уязвимости и проблемы в бизнес логике имеют несколько разный характер появления.
                Уязвимости да действительно появляются из-за человеческой невнимательности. А вот проблемы в бизнес логике, чаще появляются из-за проблема коммуникации между людьми. Программист их намеренно делает думая, что так и надо.
                Тут же возникает вопрос о специалистах которые хорошо шарят не только в программировании но и в области той науки для которой он пишет софт, а это очень часто редкие люди. возможно стоит пойти дальше и пересмотреть подготовку специалистов, убив еще 2-3 десятка лет.
                В любом случае верификация кода на очень быстро развивающихся железках (я не говорю о баловстве с ПК) — это очень проблематично.
                • 0
                  1. 4 года для 12 человек, возможно это параллелится (раз работал не один, а 12, то вероятно это так), это не так много за такой уровень надёжности. Если бы это было международным проектом, то уже был бы верифицированный весь стек технологий для разработки.
                  2. Проблема с корректностью требований не решается верификацией, это я отметил, но с требованиями проблемы в бизнесе, а в медицине, авиации, космосе, АЭС требования вынуждены формулировать максимально точно (иначе оно бы и не работало).
                  3. Да, специалисты нужны другого уровня, не обезъянокодеры, а математики-программисты. Да, нужно начинать их готовить, если этого не делать, то так и будем терять космические аппараты с бешеной стоимостью из-за программных ошибок, проводить некорректные исследования из-за багов в МРТ и т.п.
                  • 0
                    Анонс свежего ядра 4.8:

                    >> В новую версию принято более 13 тысяч исправлений от примерно 1500 разработчиков, размер патча — 41 Мб (изменения затронули 11303 файлов, добавлено 627751 строк кода, удалено 278958 строк).

                    вопрос: сколько людей и сколько времени будет проходить верификация только нового кода?

                    8700 строк кода — 12 человек — 4 года
                    348793 новых строк кода — ? человек — ? лет

                    дополнительно учитываем, что сложность верификации совсем нелинейна относительно объема кода (лично я допускаю что ближе к экспоненте)

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

                    p.s. сам регулярно прогоняю статический анализ по своему код, но это далеко не верификация, так как она будет не просто дорого, а очень дорого, проще переписать 10 раз с нуля под изменившиеся требования, чем 10 лет пилить морально устаревшее решение
                    • 0
                      Монолитное ядро пока нет шансов верифицировать, да и не нужно, а вроде старался это отметить — первоочередная задача это верифицированное микроядро для встраиваемых систем, и к счастью оно уже есть, можно двигаться дальше.
                      • 0
                        вот тут подходим к другому пункту:
                        верифицированный L4 это по сути минимальный гипервизор, который почти ничего не умеет.

                        В самом linux kernel от ядра как таковое совсем малый процент
                        первое место по объему это драйвера
                        дальше уже arch (все-таки количество поддерживаемых архитектур зашкаливает, сравните с seL4 который 4 вида arm и одни ia32 тянет)
                        и третье место за fs.

                        то есть формализовать только какой-то subset от ядра не проблема даже для монолита.
                        а вот формализовать все ядро действительно нету шансов

                        к тому же если посмотрите на последние уязвимости-ошибки, то окажется что по отдельности они не несут никаких деструктивных вещей, зачастую это даже ожидаемое их поведение, но вот грамотное построение цепочек из 10-15 таких недоуязвимостей создают большую дыру и тут даже верификация и микроядро не поможет, так как каждое из действий будет считаться допустимым, а истинная проблема возникнет на стыковке и объединении всех модулей
                        • 0
                          По идее именно гипервизор, да несколько драйверов нужно верифицировать для конкретной архитектуры и писать на чём-то вроде си, а всё остальное на условном кроссплатформенном хаскеле нужно писать (и его компилятор верифицировать для архитектуры) и его верифицировать будет проще благодаря математичности языка.
                          Но конечно в сфере о которой я говорю не будет такого зоопарка архитектур, ФС или устройств.
                          • +1
                            «Блажен, кто верует, тепло ему на свете!»

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

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

                            иногда проще поступить по принципу эрланга: если что-то падает, дай ему упасть.

                            Но в нашем случае продолжаем работать и принимать решения уже на оставшихся данных, так как любая физическая сущность всегда может упасть или начать возвращать неправильные данные (можете посмотреть количество сбоев обычной RAM в датацентрах, интересная статистика, посмотрите на последние уязвимости Rowhammer), то есть ваша программа формально будет вести себя правильно, но данные ей будут поступать некорректные.
                            • 0
                              > говорить, что там меньше архитектур и fs я бы точно не стал

                              но не факт, что это потому что так необходимо, скорее всего можно свести к паре-тройке вариантов
                • 0
                  Мне кажется, что кто-то не хочет понимать прочитанное, а кто-то не понимает смысла даже своего сообщения. Обратите оба внимание на то, что двенадцать человек четыре года занимались «работой по формулировке алгоритма математического доказательства». Они провели огромную работу за это время. Плодом этой работы стала «интерактивная программа Isabelle». И вот уже с помощью нее был проведен анализ микроядра. Сколько труда ушло на анализ не уточняется. Но не четыре года :) Думаю, порядка дня-двух, а может и меньше.
                  • 0
                    Нет, программу сделали не они, так что с понимаем похоже всё наоборот.
              • +1
                … но не факт, что в работе этого микроядра нет багов. Поскольку еще есть компилятор и железо.
                • 0
                  конечно, это всего лишь пример одного из кирпичиков в фундаменте надёжного ПО будущего
                  • +1
                    Угу, только на верификацию новой модели процессора будет потрачено 50 лет(там еще физ эффекты же есть, не только логика), а верифицированный компилятор будет компилировать неделями hello word.
                    • 0
                      Где-то мелькала инфа что с процессорами как раз проще (во всяком случае со схемой).
                      А есть что почитать про медленно компилирующий верифицированный компилятор?
                      • +1
                        Верифицированные вещи вообще медленные. Потому, что в некоторых случаях(в очень большом проценте) проще убрать оптимизацию, чем ее верифицировать. Например, развертки циклов и так далее. Просто вам прийдется сделать компилятор очень минимальным, убрать все оптимизации и каждую следующую версию ждать десятилетия.
                        Верифицировать схему не особо сложно. Сложно верифицировать ситуацию «в этом куске кремния нет неучтенных эффектов». Вам же его и производить прийдется на верифицированном оборудовании. Сейчас при запуске очередного техпроцесса уходят месяцы подтасовок оборудования(называемых «наладка техпроцесса»), в случае верификации вы должны ее заново начинать после любого минимального изменения неучтенного в предыдущих теоремах.
                        • 0
                          Кусок кремния сейчас это самое надёжное звено в цепочке кремний-схема-софт, поэтому возможно начать нужно со схемы и софта
                          • 0
                            https://en.wikipedia.org/wiki/Row_hammer, например
                            • 0
                              Это никак не противоречит тому что я сказал, по сравнению с количеством багов в софте ошибки аппаратного плана это мизер
                        • +1
                          > проще убрать оптимизацию, чем ее верифицировать

                          компилятор тогда быстрее будет — не будет заниматься оптимизацией
                          • 0
                            Ем? Вам же прийдется убрать и оптимизации по скорости. У вас какие-то странные представления о том, как устроены компиляторы и системы доказательства теорем.
                      • 0
                        Скорее даже не столько компиляция будет медленной, сколько скомпилированная таким компилятором программа будет медленной.
                        • 0
                          Компиляция тоже будет не быстрой, поверьте. Во всяком случае компиляция чего-нибудь современного(с библиотеками в тысячах файлов и десятками тысяч заголовочных файлов).
              • 0
                Произведем грубый расчет.
                Считается, что квалифицированный программист может выдавать 200 строк качественного, оттестированного кода в день. Таким образом, 8700 строк было бы написано 1 программистом за, примерно, 2 месяца (с учетом выходных).
                Получается, что потрачено 2 человеко-месяца на разработку и 576 человеко-месяцев на тестирование.

                На этом дискуссию можно заканчивать. Такое делается 1 раз с целью показать: «вот, смотрите, как мы можем», — но в реальной жизни это неприменимо. Хотя бы потому, что не существует необходимого количества «исследователей».
                • 0
                  Да вроде вполне пытаются применять в реальной жизни.
                • +2
                  квалифицированный программист может выдавать 200 строк качественного, оттестированного кода в день

                  Хрень полнейшая! Вы — индийский менеджер на индусскими программистами?
                  Всё зависит от задачи — можно, и две строчки за весь день выдать, если ищешь ошибку среди десятка тысяч строк, а можно и две тысячи строк за день накатать, если задача простая и ясная.
                  • 0
                    Вы точно программист? Речь о среднем значении. Понаберут по объявлениям…

                    И я посмотрю как вы 2000 качественного оттестированного кода в день сделаете без копипасты и искусственного набивания статов. Сказочники.

                    Ааа, все понятно. Уходи.
      • 0
        А потом мы слышим нытье «ой, а чего это лекарства такие дорогие».
        • 0
          Дорогие они скорее по другим причинам.
          Конечно это не удешевляет медицину, но повышает надёжность, куму нужна ненадёжная медицина?
          • +1
            использовать ненадежный МРТ сейчас за цену Х
            или его появление в 10 клиниках в мире через 20 лет за цену 1000*X

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

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

            даже с обычной жизни мы постоянно сталкиваемся с вероятностями в медицине:
            экспресс тесты на беременность/ВИЧ/диабет.
            • 0
              > ненадежный МРТ сейчас за цену Х или его появление в 10 клиниках в мире через 20 лет за цену 1000*X

              Не будет такого выбора.
              Речь не о том, чтобы остановится в развитии, а о том, что надо двигаться в правильном направлении, вот есть у нас теперь верифицированное микроядро, значит стоит использовать его в новых МРТ, а не костылить что-то своё, появится следующий верифицированный компонент (например ФС), значит новое нужно делать используя его.
              • 0
                Не будет такого выбора.
                Речь не о том, чтобы остановится в развитии, а о том, что надо двигаться в правильном направлении, вот есть у нас теперь верифицированное микроядро, значит стоит использовать его в новых МРТ, а не костылить что-то своё, появится следующий верифицированный компонент (например ФС), значит новое нужно делать используя его.

                Вы уже 10 раз это написали. Дайте пруф, что это так. И с чего вы взяли, что я, потратив очередные 48 человеко-лет на верификацию своего компонента (например ФС), разрешу вам использовать его бесплатно? Цена в 1000*Х это, на мой взгляд, даже оптимистичный прогноз.
                • 0
                  Пруф в статье — ссылка на верифицированное микроядро под gpl.
                  Это конечно один пример, но тут ситуация как с линуксом — каждому в одиночку такое пилить слишком дорого, поэтому компании-конкуренты скидываются и пилят ядро вместе, а защитой для них является GPL.
                  • +1
                    Где в статье пруф, что не будет удорожания разработки и увеличения сроков? В статье как раз пруф того, что на несчастные 8700 строк кода потратили 48 человеко-лет и это не дает никаких гарантий отсутствия программных ошибок.

                    Это конечно один пример

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

                    Дайте расчет или пример того, сколько придется угробить ресурсов для десятка миллионов строк кода. Только не надо сказок про то, что мы сделает 100500 финтифлюшек, протестируем каждую и это будет гарантировать, что все вместе они заработают как надо. Не позорьтесь.
                    • 0
                      > Где в статье пруф, что не будет удорожания разработки и увеличения сроков?

                      Я вроде пояснил уже, что если верифицированные компоненты будут создаваться не в рамках конкретных продуктов, а параллельно, то они не будут замедлять их развитие, и не сильно будут увеличивать стоимость т.к. затраты будут распределяться по большому количеству продуктов в которых они используются.
                      Так, например, весьма большая стоимость свободных дистрибутивов не приводит к дороговизне домашних роутеров построенных на них.
                      • +2
                        Вы раньше писали, что Вы не специалист в этой теме. По-моему, на этом можно и поставить точку в дискуссии.
    • 0
      Господа, а давайте-ка вспомним, что многие из нас называются «инженерами-программистами» или «software engineers».
      А ещё вспомним, что раньше, в 19 веке, среди инженеров — мостостроителей, было принято становиться на лодке под построенным мостом, когда по нему пускали первую нагрузку (поезда, телеги).
      Так вот, ежели заставить разработчиков софта для МРТ и авионики на себе испытывать эти установки, ответственность сама по себе возрастёт (никто не захочет умереть от своего изделия).
      То есть, банально восстановим принцип персональной ответственности инженеров за свои изделия.
      • 0
        Отвечал на это тут
    • 0
      С МРТ нудачный пример, он не может поджарить физически.
      • +1

        Жарить с помощью МРТ сложно, но магнитные поля очень сильные: http://abcnews.go.com/US/story?id=92745 "there have been "hundreds or thousands" of incidents where objects became magnetized and attracted to MRI machines .."
        http://thechart.blogs.cnn.com/2011/10/26/dont-get-hurt-by-an-mri/ Projectiles, Burns (“If there are electrical conductors like an EKG lead (on the body) it becomes an antenna and can pick up the RF and concentrate it.”), Hearing loss ("Gilk compares getting a scan to standing near a jet aircraft."), Implants and medical devices .."Coming in contact with the inside of the MRI tube can lead to burns."

        • +1

          http://medicalphysicsweb.org/cws/article/opinion/48264 Jan 10, 2012 MRI safety: accidents are not inevitable


          FDA's medical device accident database, MAUDE… showed that reported MRI accidents in the US have risen over 500% from 2000 to 2009. During that same time period, according to market research firm IMV, the overall number of administered MRI exams increased by approximately 90%.… three categories: burns, projectiles and hearing damage.… burns caused by electrically conductive materials in the bore with the patient; burns caused by proximity to/contact with active RF elements; and resistance to electrical currents generated in the patient's own body as a result of large calibre tissue loops. ..

          http://cds.ismrm.org/protected/09MProceedings/files/Fri%20A18_08%20Sawyer.pdf "Burns
from
 RF 
Electromagnetic
 Fields ..."


          Был еще такой одиночный случай в Индии из-за магнитного поля: http://www.dailymail.co.uk/news/article-2890088/Two-hospital-workers-spend-FOUR-HOURS-pinned-MRI-machine-metal-oxygen-tank-catapulted-room-device-s-giant-magnet-turned-on.html — "Two hospital workers… pinned to MRI machine by metal oxygen tank… India … Normally the incident could have been over within seconds, but the machine's emergency shut-off switch failed to work… Later reports suggested the switch had been disabled so it could only be operated by GE employees. A GE spokesman declined to confirm or deny that"
          Кнопка экстренного "размагничивания" не отключила магниты по неясным причинам. Известно, что аварийный останов может потребовать длительного ремонта и замены газов на десятки тысяч долларов: http://www.auntminnie.com/index.aspx?sec=ser&sub=def&pag=dis&ItemID=110120 "magnet rundown units (MRUs), which are designed to initiate a controlled quench and turn off the magnetic field… Such shutdowns are only intended for extreme emergencies and can put an MRI magnet out of commission for a week or more and cost up to $30,000 to replace lost helium"
          Последовал отзыв и доработка: http://www.auntminnie.com/index.aspx?sec=ser&sub=def&pag=dis&ItemID=110120 "In GE's case, a scanner's magnetic rundown unit may not actually be connected to the scanner, according to the FDA recall notice.… MRI scanners in India had been modified by service personnel or by equipment users to disable the magnet rundown unit"


          Безумные эксперименты со списанным МРТ — https://www.youtube.com/watch?v=6BBx8BwLhqg (крупные железные предметы), https://www.youtube.com/watch?v=9SOUJP5dFEg (quench, при котором выкипает жидкий гелий)

    • 0
      А что стоит наказания одного раздолбая, если выпущеный серийный аппарат МРТ, например, поджарит пару десятков человек?

      Такое уже было, мне известен как минимум один прецедент (правда не мрт конкретно, но суть та же)
      • 0

        При УЗИ беременных сканер Тошиба SSA-660 мог пережаривать плод:
        "Локальное увеличение температуры пациента… не показывалось из-за ошибки в ПО".
        http://webcache.googleusercontent.com/search?q=cache:7rJ0CGtgQmsJ:https://www.swissmedic.ch/recalllists_dl/00278/Vk_20060104_06-e2.pdf%2Blocal+increase+patient+temperature


        "not displayed even if the value is 0.4 or more in 2D mode (B mode) due to a software error."


        2) на хабре кто-то в комментариях писал про своего знакомого московского главного админа процессингового центра банка. Который сразу же снимал наличку со своей пластиковой карты в день зарплаты, видимо ожидая прилёта разрушительных "дятлов" с минуты на минуту :)


        3) Тут же в блоге мегафона написано про их страх насчёт облысения от СВЧ в собственных тестовых экранированных комнатах.


        4) анекдот: "С тех пор, как я начал водить машину, я стал осторожнее переходить дорогу."

  • +1
    Думаю, для того чтобы земная цивилизация устойчиво развивалась

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

            о защите от техногенных катастроф

            Так аппараты или катастрофы? Упавшая ракета разве что дом какой может поломать.
            • 0
              И то и то конечно, параллельно несколько веток потерял нить. Касательно техногенных катастроф, можно представить например ситуацию когда интернет стал основополагающей инфраструктурой цивилизации — ничего без него не работает, врачи не могут оперировать (не каждого пациента привезёшь к нужному хирургу), экономика не работает — ничего нельзя купить без сети (без доступа к блокчену или банку), образование не образовывается т.к. ехать за тридевять земель к нужным преподавателям никто не хочет, да и сами преподаватели частино живут не пойми где и т.д.
              Можно конечно вернуться в каменный век для надёжности, а можно сделать технологии лежащие в основе интернета столь надёжными чтобы никакие хакеры не могли остановить жизнь цивилизации.
              • 0
                Написали мы софт, верифицировали, а потом
                1) трактористы Васи порвали экскаватором оптику (реальный случай пропадания аплинка между РБ и Россией, в тот момент там свыше 50% всего внешнего канала было, сколько рвут кабелей океанических вообще помолчим).
                2) ударили молнии и вторая половина датацентров легла (случай с амазоном)

                Распределенные технологии, такие как интернет, по определению строятся на ненадежных системах, чем больше узлов в системе тем выше вероятность отказа. Поэтому для интернета стоит задача другая: как из ненадежных элементов построить достаточно устойчивую систему. Отмирание отдельной клетки не убивает организм (рак отдельная песня, но и с ним частично борются), выпадение одного сервера не ложит yandex/google/facebook (для них вылеты целиком стоек никак не сказываются на работе, даже падение целого датацентра не остановит работу). Те же DDoS это полностью правильная работа, но датацентр можно положить, тут не спасет никакая верификация.

                Поэтому отдельные части верифицировать можно, но чем крупнее система, тем больше нужно полагаться на общую устойчивость, а не на то, что у нас каждый элемент будет работать правильно и идеально и никогда не сбоить.
                • 0
                  Речь не о защите от отмирания одной клетки, а скорее об устойчивости к вирусу могущему поразить все или значительное количество клеток.
                  • +1
                    и верификация с математикой нам тут ничем не помогут, так как они не спасают от аппаратных сбоев, они не спасают от направленной атаки (Rowhammer уже приводил), они не спасают от направленного внедрения (когда человек сам запускает тот же вирус или он оказывается установленным еще на заводе изготовителе).

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

                    NASA имеет бюджет, любой спутник или ракета имеет бюджет, поэтому иногда возможно рискнуть и попытаться запустить сейчас с вероятностью неудачи в 0.001% чем пропустить запуск и ждать следующих 4-5 лет для появления окна запуска. В случае неудачи у вас есть риск строить такой же аппарат еще 8 лет, но это сознательный риск.

                    Не задумывались почему даже на Curiosity обновление прошивки заливали уже после достижения Марса: в момент отправки оно просто не было готово, не хватает ресурсов.
                • +1
                  Так эта «общая устойчивость» — тоже алгоритмы и их тоже можно верифицировать. Точнее даже в распределенных системах только их в первую очередь и имеет смысл верифицировать, сам Лесли Лампорт главный адвокат такого подхода с его TLA+.
                  • 0
                    Вот, мы верифицируем общую устойчивость и я с этим полностью согласен и пытаюсь это донести.

                    Верифицировать и гарантировать работу ВСЕХ составляющих дорого, долго и не имеет смысла.
  • 0
    Почему земляне делают глючный софт и железо

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

    надо иметь математическое доказательство этого утверждения

    Вообще-то надо просто проверить, как работает. В разных ситуациях и с разными данными.

    Математическое обоснование тут не подходит, т.к. задача слишком сложная и нелинейная. Строгого решения вы просто не найдете.
    • +1
      И сразу же сроки проверки простейщей программы стремятся к бесконечности! Это как проверить устойчивость алгоритма хеширования на предмет коллизий. Всего каких-то 256 бит, и времени всей вселенной на нынешних скоростях не хватит чтобы проверить все варианты. Тут как раз математическое обоснование выглядит гораздо более простым и реализуемым.

      Простейшая, даже самая очевидная программа — X = A + B где A и B — целые 32-битные числа. Количество вариантов которое надо проверить чтобы выдать положительный вердикт — 2^64 степени, при вычислительной мощности процессора 1000МFLOPS время на тест такой простейшей программы полным перебором составит не менее 18446744073 секунд, или почти 585 лет непрерывной работы. И это для простейшей очевидной программы, работоспособность которой легко доказать.
  • +1
    Да, соглашусь 2 и 3 проблемы, можно скорее всего закрыть предложенным способом. А как насчет первого? Идеальной защиты от дурака не напишешь. Люди в свое глупости(ну или лени) очень изобретательны.

    И по-моему Вы упускаете один аспект или как вы их называете причину, как насчет того что человек в силу своей несовершенности не может учесть всего? Взять ту же АЭС, сможете перечислить все возможные варианты событий, которые могут произойти и которые надо учесть в ПО? Мы в обычной жизни не всегда можем все варианты просчитать, что уж говорить о сколько-нибудь серьезных проектах. И тут уже проблема не в глючности, а именно в том что все это для начала учесть, а потом и запрограммировать, а потом еще и проверить.
    • 0
      Да, я отмечал, что проблему корректно сформулированных требований это не решает, но во-первых, это не отменяет нужности верификации, во-вторых, в проектах критического уровня требования всё же стремятся сделать (благодаря этому АЭС работают, самолёты летают) и самое главное — если мы вдруг обнаружили ошибку в требованиях и исправили и верифицировали, мы точно знаем, что улучшили систему, уверены что исправляя не внесли новых багов т.е. мы поднимается по лестнице развития, а колеблемся около горизонтальной оси исправляя одно и ломая другое.
      • 0
        А как проверять тех кто проверяет?
        • 0
          А как с сейчас проверяют? Речь же не о волшебной палочке, а об улучшении одной составляющей процесса (проверки программ), остальные остаются теми же.
          • 0
            Ну т.е. Вы переносите ответственность за корректность программы на какой-то другой уровень.
            А корректность самих «проверяльщиков» (будь то ПО или люди) как проверить?
            Почему проверенная ими программа будет более корректной если мы не можем доверять проверяльщикам?
            • 0
              Да никак нельзя проверить проверяльщиков, это будет бесконечная цепочка проверки, поэтому на практике ограничиваются двумя звеньями — одни делают, другие проверяют
        • 0
          Как насчёт варианта «несколько незавимых (т.е. каждая из них написана с нуля) проверяльщиков проверяют код друг друга»? Скажем программа-проверяльщик А проверяет саму себя и программы-проверяльщики Б и В. А те в свою очередь самих себя, друг друга и саму програму А. Строго говоря вероятность ошибки останется, но она, скорее всего, будет пренебрежимо мала.
  • –1
    Скажите, а может более оптимален такой вариант? Дублировать программы от разных программистов?
    Допустим, надо вычислить высоту над поверхностью. Расчёт высоты ведётся не одной подпрограммой, а тремя одновременно, но три подпрограммы разные по алгоритму и писались разными программистами. Если объёмы устройств позволяют, то компьютеров физически три. Управляющее устройство срабатывает, если от двух и более алгоритмов поступили одинаковые цифры.
    • 0
      А если не поступили, то летательный аппарат, стало быть, теряет управление и зависает в воздухе, ожидая сервисной команды?
    • 0
      Вариант хороший, но в 3 раза дороже, чем обычные решения. Для военки и космоса наверное подойдет. С другой стороны для достаточно сложных случаев такой подход не сработает, грубо говоря облететь препятствие можно и правильно слева или справа, сверху или снизу, будет ситуация как в той басне, все тянут в свою сторону и все правы.
    • 0
      Так иногда и делают в критичный областях типа авиации и космоса, но даже это не всегда помогает
    • 0
      так было на Шатле 4 одинаковых компьютера и 1 совершенно другой от другой компании
      и тоже был какой-то инцидент
    • 0
      Диверситетное программирование называется
      Ну или не «ди», а N.
      • 0
        Судя по гуглу — мультиверсионное или N-версионное программирование
        Есть даже что-то на хабре
  • 0
    Интересно одно — с точки зрения современной математики это реализуемо? Как минимум у машины Тьюринга есть проблема останова неразрешимость которой вполне себе доказана, так что тут есть фундаментальные ограничения. Было бы очень интересно узнать мнение эксперта в этой области.
    • 0
      Судя по ссылкам на ядро L4 которые я привёл это не только реализуемо, но и реализовано.
    • +2
      В языках программирования с поддержкой зависимых типов очень просто решается проблема останова.

      Мы просто разрешаем существовать только гарантированно выполнимым функциям. Проворачивается это каким-нибудь таким способом:

      recursive :
        A → B:(A → U) → C →
        order:TotallyOrdered C →
        HasLowerBound C order →
        IsDiscrete C order →
        extract:(A → C) →
        
        (a:A →
         (x:A → Lesser order (extract x) (extract a) → B x)
         → B a)
         
        → a:A → B a


      Мы хотим получить функцию A → B (принимающую значение типа A, возвращающее значение типа B), в которой хотим использовать рекурсию.

      Для этого мы просим наличие типа C, элементы которого линейно упорядочены, имеющий нижнюю границу (меньше которой элементов не существует) и для которого выполняется дискретность (есть гарантии того, что между двумя любыми элементами конечное количество элементов, т.е. например, это целые числа, а не рациональные).

      И ещё просим функцию A → C, которая «оценит вес текущего значения A».

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

      И все наши программы будут завершаться когда-нибудь (если никто не будет вычислять что-нибудь невероятно долгое, вроде функций Аккермана — ограничивать по времени выполнения куда сложнее, придётся описывать виртуальную машину и ограничивать количество выполняемых инструкций).
      • +2
        Ещё немного уточню, почему именно так. Когда мы создаём функцию f, внутри неё у нас нет доступа к f и мы не можем сделать рекурсивный вызов. Можно двумя путями дать этот доступ — или передавать её в «конструктор функции», или использовать Y-комбинатор.

        Первый путь будет означать, что желая создать функцию f:(A → B), мы будем иметь F = (F → A → B).

        Мы только что создали рекурсивный тип. Рекурсивные типы полезны (к примеру, тип списка — рекурсивен: List T = Unit + (T, List T), но не все из них разрешены, т.к. существоние некоторых приводит к возможности получить элемент типа Ложь, в котором по определению нет элементов (т.е. получить противоречие в нашей теории, что уничтожает её целиком).

        На примере нашего F = (F → A → B): пусть A = Unit, B = 0 (0 = Ложь). Тогда f p a = p a. Мы корректно определили функцию f, которая валидна по типам, но, к сожалению, приняв значение типа Unit (которое у нас всегда в наличии по определению), мы получим противоречие.

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

        С Y-комбинатором те же дела, это просто обобщённая функция, тип которой является запрещённым рекурсивным.
        • 0
          у меня есть правила, какие типы разрешены, а какие нет, но не буду их здесь описывать, если нужно — спрашивайте

          А какие правила помимо того, что тип не должен стоять в отрицательной позиции?
          • 0

            Тип X предоставляет A если:


            1. Равен A.
            2. Является произведением типов, один из членов которого предоставляет A.
            3. Является суммой типов, все из членов которой предоставляют A.
            4. Возвращаемое значение функции предоставляет A.

            И вот в описании типа A типы, предоставляющие A не могут быть использованы в качестве типа аргумента функций внутри этого типа.


            1. Ограничили типы `T = T → 0`
            2. Ограничили типы `T = (T, AnyOtherTypes) → 0`
            3. Ограничили типы `T = (T + (T, AnyOtherTypes)) → 0`
            4. Ограничили типы `T = (Unit → (T + (T, AnyOtherTypes))) → 0`

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


            A = B + C
            B = 1 + C
            C = 1 + B

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

  • –1
    Это проблема цивилизации. И будет до тех пор, пока Я доминирует над МЫ.
    • 0
      ну, у китайцев МЫ…
    • 0
      Пока у смертных разработчиков преобладают корыстные и личные мотивы, они будут «ваять» тлен и хлам на радость хакерам, дятлам и в топку энтропии.
      Но в природе существуют программы биороботов, веками не устаревающих и без побочных эффектов.

      «Верный мотив – работа на Общее Благо и Служение Жизни.
      Неверный мотив – всё, что заставляет вас преследовать любые цели, принадлежащие физическому плану: слава, деньги, почёт, получение удовольствий, удовлетворение желаний.»
    • +1
      За доминированием «мы» над «я» вам к муравьям и термитам. Они, кстати, освоили строительство, животноводство, сельское хозяйство, разделение на касты и т.д. Глядишь, через пару миллиардов лет и до программирования дорастут.
  • +2
    Формальная верификация — это совсем не 100% гарантия, что программа работает корректно. Это способ перепроверить программу лишний раз, анализируя ее в другой плоскости другим методом, тем самым выявляя дефекты и уменьшая вероятность не раскрытых дефектов. Но не стоит забывать, что пока этим занимаются «земляне», они в доказательствах тоже могут допустить ошибки, некорректные допущения и т.д. История самой математики знает далеко не единицы таких ошибок. Поэтому верификация позволяет уменьшить частоту дефектов в коде на один-два порядка, но не избавиться от них полностью.

    Важно понять, что смысл не в том, чтобы избавиться от всех дефектов, а в том, чтобы найти какой-то подход, который позволит избавиться от многих дефектов минимальными усилиями с учетом современных реалий. Формальная верификация тут не пройдет.
    • 0
      Формальная верификация это самый надёжный из доступных нам способов проверки.
      А касательно минимизации влияния человека как раз свежий пост.
      • +2
        Нам не интересна проверка корректности ради проверки корректности. Нам интересно избавление от проблем, вызванных дефектами и формальная верификация в этом далеко не самый надежный способ, не стоит заблуждаться. А лишь один из инструментов повышения надежности, причем довольно узкоспециализированный.
        • 0
          с вашими «аргументами» не поспоришь
          • +1
            zzzcpan на самом деле говорит об базовых вещах. Таковы фундаментальные свойства всех формальных систем в отношении их интерпретаций. Если на пальцах, априорные тесты могут как угодно показывать, что программа их проходит в момент запуска тестов. Но они не могут гарантировать, что программа при эксплуатации делает именно то, что вам в данный момент времени хочется, чтобы она делала в текущем окружении.

            Другими словами, наличие тестов не может поменять суть надежности, как вероятностной оценки, на что-то иное.
            • 0
              о какие тестах речь? я вроде ни о каких тестах не говорю
              • +1
                Написал «тесты» на автомате. Как вы могли понять, формальной верификации все это относится в той же степени. Представьте программу для игры в шахматы, и как факт наличия формальной верификации кода будет влиять на исход конкретной партии.