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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    Подробнее
    Реклама
    Комментарии 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
                                                                                              Эволюция — выживают сильнейшие.
                                                                                              Известное заблуждение: на са