Но при этом все привыкли к тому, что ПО на их устройствах работает непредсказуемо, через раз, что даже установка самых последних обновлений не гарантирует отсутствия проблем с безопасностью, что часто в открытом, массово используемом коде находят ошибки существующие там много лет, что даже у крупных и «технологических» компаний бывают сбои и утечки данных, что космические аппараты разбиваются или теряют часть функциональности вовсе не из-за козней инопланетян (марсиане клянутся что не сбивали ExoMars).
Хотелось бы рассмотреть причины и возможные пути решения этой планетарной проблемы.
- Непрофессионализм и некомпетентность исполнителей — земляне, в основной массе, не научены и не приучены делать свою работу хорошо. Эта проблема стоит очень остро, и говорить о ней можно долго, но видимо надо писать отдельный пост. Тут лишь можно сказать, что настоящие профессионалы всё-таки есть, на передовые проекты должно хватать, но проблемы есть и в таких проектах, значит дело не только в этом.
- Отсутствие цели сделать хорошо/плохой менеджмент/недостаточные инвестиции — эта причина вполне вероятна в обычных коммерческих проектах, где задача стоит получить краткосрочную прибыль, а не сделать хорошо. Но это явно не про космические проекты, где цена ошибки слишком велика и в деньгах и в репутации, а затраты на разработку по некоторым оценкам в 160 раз выше обычной коммерческой разработки, однако также без гарантии надёжности.
- Использование неподходящих инструментов/попытка молотком шлифовать линзу — вот эта причина мне кажется главной и о ней я буду говорить далее. Именно из-за неправильного подхода к решению задач честные программисты никогда не говорят «Да, оно работает», а говорят «Вроде работает», «Должно работать».
Когда земляне берутся за самые сложные из стоящих перед ними задач, вполне логично было бы применять для их решения самый лучший из имеющихся инструментов.
И этот инструмент, это точно не человеческий мозг, мозг homo sapiens это как раз инструмент из серии «вроде работает» и не стоит этому удивляться, всё-таки эволюционировал он для совсем других задач, поэтому даже самый крутой профессионал может сделать тупую ошибку по куче причин.
Конечно, собрав вместе много хороших мозгов, можно улучшить результат, но без хорошего инструмента и все мозги планеты не достигнут того, что уже достигнуто.
Чтобы понять, что это за волшебный инструмент стоит попробовать ответить на вопросы вроде «Почему небоскрёбы не разрушаются под своим весом или на ветру?», «Как наши космические аппараты добираются до цели в необъятных просторах космоса?», «Как мы умудряемся надёжно пересылать данные по ненадёжным каналам связи?», «Откуда взялись надёжные методы шифрования?» и так далее и тому подобное.
Ответ на все эти вопросы один, этот инструмент — математика. Математика это магия современного мира, для непосвящённых такие артефакты как Zcash или CryptDB, да и, ставшее привычным, асимметричное шифрование выглядят как волшебство, хотя это лишь применение этого мощного инструмента.
Для того, чтобы сказать — «Да, программа работает как требовали», надо иметь математическое доказательство этого утверждения, к сожалению я не специалист в этой сфере, но насколько знаю процесс этого доказательства достаточно сложный, но это не должно быть препятствием по следующим причинам:
- Иного пути нет, наши системы усложняются, новые слои опираются на старые, но к сожалению это не очень надёжный фундамент.
- Доказывать нужно небольшие программы (юникс-вей).
- Доказывать нужно лишь программы критичные для безопасности надёжности. Можно не доказывать корректность офисного пакета, но микроядро ОС или библиотеки шифрования должны быть доказаны.
- Доказывать не обязательно существующий универсальный софт, не обязательно это будет ОС общего назначения, возможно что-то более простое, без свистелок, но максимально надёжное для медицины, транспорта, АЭС.
- Использование строго математических языков программирования может снизить затраты на доказательство (Haskell?). Да, они могут быть в чём-то сложнее обычных ЯП, но их сложность соответствует сложности задач которые необходимо решать.
- Не обязательно доказывать сразу всё, но шаг за шагом можно построить доказанную инфраструктуру для построения надёжных систем.
Конечно доказательство программ не избавляет нас от необходимости точно формулировать требования, но думаю это решаемая задача, тем более, что в некоторых случаях (вроде библиотек шифрования) сами требования тоже формализованы.
Думаю все хотели бы, чтобы на АЭС, в медицинском оборудовании и подобных местах работало абсолютно надёжное ПО.
Не буду утверждать, что надо было давно это сделать, отрасль бурно развивалась, много чего значительно поменялось, но сегодня, с моей точки зрения, отрасль достаточно зрелая для того чтобы начать наводить порядок.
Есть новые классы задач вроде квантовых компьютеров и специализированных процессоров для нейронных сетей, там всё только начинается. Но развитие этих отраслей не отменяет нужности классического подхода — у всего свои задачи.
Земная цивилизация уже сейчас очень зависима от надёжности компьютерных систем и чтобы не вздрагивать ночью от шума крыльев залётного дятла, надо искать решения повышающие надёжность.
Отдельно стоит сказать про нейронные сети, нейронные сети это попытка копировать мозг со всеми его плюсами и минусами, решение на нейронных сетях содержит те же проблемы что и человеческий мозг, поэтому их нужно применять только там, где мы не знаем как решить проблему с помощью формального алгоритма работающего абсолютно надёжно.
Думаю, для того чтобы земная цивилизация устойчиво развивалась ей пора задуматься над надёжностью своей инфраструктуры, касательно ИТ мне это видится так — нужно выбрать/создать высокоуровневый математический язык программирования и начать создавать полностью на нем (без спрятанных под капотом сишных либ) наиболее критичные программы с последующим их доказательством. Вполне вероятно, что и аппаратная архитектура процессоров должна быть доказана и заточена под исполнение программ на таком языке (лисп-машины?).
Кто это должен делать? Не знаю, но такой же вопрос можно было бы задать на предложение всем миром писать ядро ОС, однако Linux вполне пишут, а значит варианты есть. Есть например формально верифицированное ядро seL4 (пояснения в их вики) разработанное в NICTA, если подобные проекты на станут основой для цифровой инфраструктуры будущего, то у человечества появятся шансы не пройти великий фильтр цивилизаций (кто уверен что вирус не начнёт ядерную войну?).
Планету больше не закрывали белые стаи облаков, с ее лица сползли остатки зелени и голубизны. По поверхности пробегали, искрясь и подмигивая звездами в вышине, сверкающие цепочки огней, и оттуда, как в танце сказочных фей, поднимали к небу свои лепестки, переливающиеся всеми оттенками нежнейше черного цвета, благоухающим ароматом ультракороткого излучения, пышные, пенящиеся и мерцающие своей хрупкой, утонченной красотой атомные орхидеи.
— Это чудо… чудо! О, как великолепно!
— Да. Это самое прекрасное из того, что я только видел во Вселенной…
— Наверное, планеты и существуют для того, чтобы распуститься только один раз… Но разве этого мало?..
«Когда расцветают бомбы»
ОБНОВЛЕНИЕ: В процессе обсуждения в комментариях созрела важная мысль — для того, чтобы внедрять в критичных сферах верифицированное ПО вовсе не обязательно останавливать текущую разработку, нужно параллельно создавать свободные верифицированные компоненты, а по их готовности новые вещи делать с их помощью, например вышеупомянутое микроядро seL4 для встраиваемых нужд уже есть, а значит нужно его использовать везде где он подходит. И работать над другими компонентами.
Комментарии (302)
vkegdzoy
17.12.2016 21:06+7Все причины можно уместить в одну: Коммерциализация. Даже полёт на луну это продажа идеи конкурирующей с другой.
Neuromantix
17.12.2016 21:13Мне кажется, дело еще и в том. что вместо одного «железячника» для хардварного решения части проблем проще нанять 10 «индусов» для ее софтварного решения.
Например, я столкнулся с проблемой — нужен был счетчик импульсов на 12 разрядов. Большая часть микросхем мелкой логики, на которой его можно построить, уже снята с производства. И на меня смотрели как на идиота — мол, делай на МК и все. Один корпус вместо двух десятков и прочее. Но мне нужна была абсолютная устойчивость (помехи, МК может виснуть, железное решение, стоявшее там до этого не висло при грамотной экранировке совсем и никогда), плюс еще некоторые хитрые параметры. Почему «железячные» решения исчезают в угоду софту — мне непонятно. Но это меня не радует.
worldmind
17.12.2016 21:19+3Универсальность видимо, проще делать одну железку на все случаи жизни, чем сотню разных и это не проблема если схема этой универсальной железки математически надёжна.
Neuromantix
17.12.2016 21:22+1Проще для производителя — может быть, проще для пользователя — не уверен. Специализированное устройство всегда эффективнее и удобнее «комбайна». построенного на компромиссах.
worldmind
17.12.2016 21:31+2Да в какой-то момент эффективность универсального решения может стать столь высокой, что практической разницы со специализированным не будет.
Ну и пользователю проще изучить одно решение чем каждый раз доки читать. (если что минус не мой)
Sun-ami
17.12.2016 23:17+4Счётчик на МК может быть менее чувствителен к помехам, поскольку у него нет множества достаточно длинных проводников, соединяющих логические элементы, на которые может быть наведена помеха. И если частота импульсов низкая — его можно снабдить множеством программных средств самоконтроля, при помощи которых можно добиться высокой вероятности его правильной работы даже в случае, если в МК произойдёт сбой.
Neuromantix
18.12.2016 11:12+1А в дубовой логике оно просто работает десятилетиями без средств самоконтроля и иных костылей.
Vcoderlab
18.12.2016 12:02Максимум, что грозит устройству на логике, — перескок через несколько «тиков» счёта или сброс в начальное состояние и новый отсчёт с нуля. Иными словами, помеха может изменить текущее состояние устройства, но не может нарушить его нормального функционирования.
При этом МК может творить всякие чудеса от перескока на совершенно неожиданную ветку программы вплоть до полного зависания, выдернуть из которого его может только отключение питания.
Sun-ami
18.12.2016 12:47Если использовать brown-out детектор и watchdog-таймер — МК как правило тоже не творит чудеса, а сбрасывается, и даже не теряет при этом данные и может продолжить счёт — валидность данных можно проверить по их копии. А сброс в начальное состояние, факт которого даже не фиксируется — это не нормальное функционирование.
Vcoderlab
18.12.2016 16:33+2Ключевое слово — «как правило».
К сожалению, в реальности и с включенным watchdog таймером МК порой намертво зависает. Реже, чем без него, но всё-таки зависает.
Alexeyslav
19.12.2016 12:15+3Точно так же может зависнуть и аппаратный счетчик — триггерный эффект по входу из-за наводки и вход не работает до передёргивания питания(в лучшем случае).
Возьмём к примеру классический счётчик джонсона(561ИЕ8), который может иметь запрещённые(невалидные) состояния, наведённые помехами и только специально спроектированная схема позволяет счётчику выйти в одно из рабочих состояний за конечное количество тактов.
Если взять более сложные схемы на логике(Привет ПЛИС) то там так же достаточно много «программных заморочек» где что-то может пойти не так. Даже обычный триггер можно манипуляциями входных сигналов ввести в невалидное состояние. Попробуйте узнать для чего вообще придумали двойные(с двойной защелкой) D-триггеры. И всё это является примером того как в программах преодолевают сбои, только на аппаратном уровне. И даже двойная защёлка не убирает аппаратную проблему простого триггера а только лишь уменьшает вероятность её возникновения.
А ещё есть race condition…
Fandir
19.12.2016 11:46ПЛИС вам чем не угодили? Рассыпуха уже и правда прошлый век под вашу задачу хорошо бы подошла любая ПЛИС.
Alexeyslav
19.12.2016 17:16+1Пожалуй, у большинства ПЛИС больше проблем будет даже чем с МК. Уж больно они чувствительны к нагрузкам на выходе, наводкам на воде вызывающих порой тиристорный эффект и чистоте питающего напряжения. А ещё, что более ужасно, в эквивалентных схемах(рассыпуха vs ПЛИС) в ПЛИС задействовано больше элементов в цепочке снижающих надёжность всей конструкции.
Neuromantix
19.12.2016 23:57Еще одна проблема — «время жизни» чипа. То, что выходило 5-7лет назад, давно снято с производства С ПЛИС в этом отношении проще МК (прошивку можно залить в разные плис, чуть подправив), но плату все равно придется переделывать.
goodbear
17.12.2016 21:38+3Земляне делают глючный софт, потому, что сами глючные, довольствуются глючным софтом, применяют при производстве глючные подходы, наказывает кого попало, а не того кто наделал глюков и важно им совсем не безглючность а что бы было быстро сделано, свиду работало и клиент быстрее заплатил.
maxpsyhos
17.12.2016 21:57+19Господа, опомнитесь! Кода это были те светлые «не коммерциализированные» времена, когда ошибок в программах не было? Вы случайно планетой не ошиблись?
В прикладных программах всегда были баги. В картриджах для игровых приставок (ПЗУ, новую версию не накатишь) были баги, в операционных системах со времён их появления были баги, в микрокодах процессоров были, да даже в топологии процессоров были баги.
На военных спутниках и самолётах были баги, и это несмотря на смехотворный по нынешним меркам объём кода, простой как топор процессор и 10 колец оцепления со всеми существующими способами их устранения.
Не было никогда безглючного софта и не будет никогда. Это фундаментально невозможно.
А тем, кому не нравится «коммерциализация», можно предложить альтернативу — вы будете покупать железо, которое стоит как ваша квартира? Игры не за 4 тысячи, а за 40? Пустой интернет, потому что все профессора информационных технологий в стране завалены заказами на год вперёд. Всеми 10-ю заказами? Прикладной софт, не обновляющийся десятилетиями по этой-же причине? А то, что его ещё и меньше будет на пару порядков?
И всё это ради того, чтобы частота возникновения ошибок сократилась с «1 раз в неделю» до «1 раз в год».
На сам-то деле всё проще. Программа (и железо) нужна чтобы решать какую-то задачу, у неё нет самоцели быть правильной. Глюков, багов и недоработок в ней будет ровно столько, сколько экономически обоснованно. Всегда есть предел, после которого затраты на дальнейшее улучшение начинают превосходить полезный эффект от этих изменений.
fenrirgray
17.12.2016 22:19-3Вы не правы. Безглючный софт фундаментально возможен. Я могу это доказать, к примеру вывод какого-нибудь «hello world» — вполне себе софт, и там не будет багов, негде просто. Если сильно заморочиться идеей безглючности можно этот «hello world» на ассемблере написать, дабы избавиться от лишних прослоек в виде компиляторов/интерпретаторов.
Для написания более сложного безглючного софта существуют специальные методики(см. formal verification).
Другое дело, что методики не защищают от архитектурных или логических ошибок.
С чем я могу полностью согласиться, так это с тем, что безглючный софт комерчески совершенно не целесообразен.
sumanai
17.12.2016 23:45+5Если сильно заморочиться идеей безглючности можно этот «hello world» на ассемблере написать, дабы избавиться от лишних прослоек в виде компиляторов/интерпретаторов.
Для багов остаётся ОС со всем букетом драйверов, прошивки железа, само железо.fenrirgray
17.12.2016 23:51-3Возмите микроконтроллер который вам будет азбукой морзе лампочкой мигать.
sumanai
17.12.2016 23:53+1Ну вот и пришли к тому, что или микроконтроллёр, бесполезно мигающий лампочками, или ПК с 4 ядрами, гигабайтами и SSD, и запущенным на нём браузером, падающим раз в неделю.
arheops
17.12.2016 23:59+3Не, мигающий микроконтроллер это сильно сложная вещь. У вас будет на «поиграть» вместо современного компьютера 3-х знаковый калькулятор.
Что убирает сразу много классов задач(те же игры становятся очень дорогими) и как результат полностью убирает экономический смысл улучшения архитектуры(и фраза деректора IBM про рынок компьютеров в размере 5 штук на планету становится правдой).
Кому нужен микроконтроллер с лампочками, если верификация его ПО потребует суперкомпьютера(ВЕРИФИЦИРОВАННОГО с верифицированным ПО), которого ни у кого нет.
ploop
18.12.2016 12:54+1Возмите микроконтроллер который вам будет азбукой морзе лампочкой мигать.
… который глюканёт при сбое питания. Попытаетесь предотвратить это событие — наткнётесь на баг аппаратной части этого контроллера (которых немеряно, почитайте даташиты в конце). Закажете партию МК без этих багов — получите мигалку космической приёмки по цене топового смартфона.
maxpsyhos
18.12.2016 03:37Максимум, что можно решить математически — это валидность программы с точки зрения языка + наличие «защиты от дурака». Но нет ни единого способа определить, что работающая программа работает правильно, т.к. она и есть наиболее полное формальное описание, как должно быть правильно.
worldmind
18.12.2016 10:08+1Ну если вы утверждаете что нет такого способа, то конечно мне придётся удалить статью и забыть словосочетание «формальная верификация»
maxpsyhos
18.12.2016 10:24«формальная верификация» — это не какой-то механизм, который можно автоматизировать для общего случая, как например статический анализ. Это индивидуальная работа по каждому конкретному случаю.
Кроме того, то что я не просто так написал «программа и есть наиболее полное формальное описание, как должно быть правильно». Если у вас верификация более проработана, чем программный код, то она фактически становится первичным исходником программы, по которому строится всё остальное. И мы снова упираемся в то, с чего начали, как проверить, что мы при верификации учли все возможные ошибки, если её результат — это самое исчерпывающее описание программы?worldmind
18.12.2016 10:27вы удивитесь, но я об этом писал в статье, и дополнительно отвечал тут
maxpsyhos
18.12.2016 12:10Да я собственно и не спорю ни с вами ни со статьёй.
Просто вы написали «есть такая метода чтобы свести ошибки почти к нулю» и началось: «а вот как хорошо раньше было», «а ведь можно же всё делать хорошо», «какуюстрануиндустрию просрали», «это всё коммерсанты виноваты».
А то, что эта метода имеет имеет астрономическую стоимость, да к тому же тоже не без изъяна, и поэтому в «повседневной работе» не особо применима, все как-то из виду упускают.
Sergey_34
18.12.2016 10:08А как насчёт?
«стиль программирования под названием формальное подтверждение. В отличие от обычного кода, написанного неформально и оцениваемого обычно только по его работоспособности, формально подтверждённое ПО выглядит, как математическое доказательство: каждое утверждение логически вытекает из предыдущего. Всю программу можно проверить с той же уверенностью, что и математическую теорему.»
https://geektimes.ru/post/282234/
Rulexec
18.12.2016 12:05+4Можно, один из них — теория типов.
У вас сейчас статически типизированные программы типизированы не полностью. Т.е. у вас в наличии функции типа«принимает массив с элементами типа T и число, возвращает элемент типа T или создаёт исключение».
А в более мощных системах типизации (где есть зависимые типы) можно иметь функции типа«принимает массив длины n с элементами типа T, число m, которое больше либо равно нуля, строго меньше n, возвращает элемент типа T».
И тогда вам нужно будет передавать в эту функцию значения типа«m меньше n», чтобы ваша программа вообще смогла скомпилироваться.
И так можно описывать абсолютно что угодно, включая то, как должны обрабатываться внешние события, хотя никто не верит.
TerraV
18.12.2016 14:09и как интересно статическая типизация должна справиться с этим, если этот массив создается в рантайме? Вы, конечно, можете возразить что сам тип массива должен включать ограничение на длину, но тогда весь код будет засран уникальными типами. Здесь массив не больше 4, там не больше 6. В третьем месте от 3 до 8 и т.д. Самое близкое к реальной жизни что я видел, это «контракты», когда на входе в метод параметры проверяются на ограничения (к примеру как у вас). Видел даже несколько библиотек для java, можно посмотреть здесь в разделе Languages with third-party support https://en.wikipedia.org/wiki/Design_by_contract
По личному опыту самое простое это использование prerequest в начале метода (к примеру из guava). Но в любом случае это не compile-time validation.Rulexec
18.12.2016 15:44Не, у нас нет уникальных типов, есть вполне общий
Массив n элементов типа T.
И никто не мешает использовать эту n в рантайме.
Просто чтобы обращаться потом к произвольным элементам массива действительно нужно будет делать явные проверки времени исполнения, чтобы получить доказательство того, что индекс действительно меньше (но если потом, к примеру, использовать числа, которые меньше проверенного, то больше проверок делать не нужно будет, ибо можно будет доказать этот факт и проверка в итоге будет только первая).
Но, например, если мы просто хотим обойти весь массив, то если мы устроим цикл от 0 до n — нам не потребуется ничего проверять, т.к. будет тривиально получить пруф того, что индекс будет меньше n, ибо нам его генерит цикл и никуда не меняет больше.
Буду дома, может накидаю какой пример кода, как именно оно будет проверяться.
senia
18.12.2016 16:30Вопрос в том насколько у вас мощная система типов. Например на 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 тут, кстати, не уникальна.
potan
22.12.2016 18:45Это умеют проверять так называемые «зависимые типы». Но ими пользоваться обычно тяжело.
К счастью, это не на столько частая ошибка, если с массивами в основном работать с помощью инетретором и отлаженных функций высжего порядка (map, fold и тп).
Deerenaros
18.12.2016 09:42О, давайте! Спустимся в процессор и будем физически доказывать его непоколебимость? Свободу от наводок палящего излучения и физической невозможностью «забыть» какой либо бит? Давайте! Спустимся в физику и будем доказывать её непоколебимость? Докажем работоспособность p-n переходов в любых условиях и приручим заведомо случайную, почему нет? Давайте! А сверху ещё останутся виртуальные машины, операционные системы реального времени и различные архитектуры процессоров, от велосипедов на ферромагинитах до 64-битных ARM Cortex A72. А ещё можно продолжить быдлокодить где быдлокодили и не лезть к серьёзным людям, занимающимся настоящей работой, навроде проектирования радиоаппаратуры и интегральных схем. Потому что душа без тела никому не нужна, а вот тело с кривой душой вполне работоспособно. Всегда есть риски, нельзя взять и уйти от них.
В любом случае, математика не идеальна. Это ещё тов. Гёдель показал, а вот что с этим делать другой вопрос. И да, она может ошибаться, теоремы могут быть ошибочны, а их предпосылки логически неверны.
Ко всему прочему, мы до сих пор не могём разрешить нелинейных дифференциальных уравнений в системе с парой десятков неизвестных (читай, энергетически оптимальный запуск ракеты), что уж говорить про тензорную и топологическую ересь.worldmind
18.12.2016 09:45На первый вопрос ответил тут https://geektimes.ru/post/283804/?reply_to=9760964#comment_9761208
А то что Гёдель доказал вам стоит почитать ещё раз, математика не может ошибаться если она непротиворечива, но при этом может быть неполна (т.е. какие-то истинные утверждения могут быть невыводимы, но это цена за точность), а вот если полна, то может ошибаться, но такой вариант видимо на практике бесполезен.Deerenaros
18.12.2016 14:43При чём тут кремний? Я говорю про фундаментальную невозможность сделать наверняка, вы говорите кремний самый надёжный. Вы говорите Гёдель доказал, что математика не может ошибаться если, я хочу заметить, что при этом в ней будут нерешённые задачи, априори. Да и банальные ошибки в доказательствах возможны, в комбинаторике постоянно опровергают доказательства.
guai
18.12.2016 18:38+1Внезапно, правильный hello world на сях не так тривиален, как может показаться :)
удивляемся, читая это http://erdani.com/tdpl/2010-12-08-ACCU.pdf с 11 страницы
black_semargl
23.12.2016 16:06Даже тут можно незаметно для себя вывести «hell world», что радикально меняет смысл…
stalinets
17.12.2016 22:27+1Вот хочу чуть-чуть процитировать Бориса Чертока, он работал с атомщиками, когда делали первую «атомную» ракету Р-5, и немного писал про то, как собирали атомные бомбы.
Нам предстояло разработать технологию совместных испытаний двух «изделий в целом» после их стыковки и весь многоступенчатый технологический план работ на стартовой позиции. Эту работу Королёв поручил молодому заместителю Воскресенского Евгению Шабарову. Почему не самому Воскресенскому? Здесь в который раз я убедился в умении Королёва выбирать людей для соответствующей задачи.
Воскресенский был испытатель высшего класса, одаренный необычайной интуицией. Кто-то метко его охарактеризовал: если бы он был лётчиком, то рисковал бы, как Чкалов. В отношениях с атомщиками партизанские действия были абсолютно недопустимы. Кроме существа дела, требовалась и его чёткая, последовательная формализация.
Что будет, если при подготовке ракета с атомной бомбой свалится у старта по причине, аналогичной упомянутому выше разгильдяйству с незакрытым баком перманганата натрия? Методика работы атомщиков предусматривала тройной контроль всех операций по сборке и испытаниям. Руководитель сборки или испытаний держит инструкцию и слушает, как испытатель громко читает содержание операции, например: «Отвернуть пять болтов, крепящие крышку такую-то». Исполнитель отворачивает. Третий участник работ докладывает: «Пять таких-то болтов отвернуты». Контролёр — представитель военной приемки — докладывает, что выполнение операции принял. Об этом делается роспись в соответствующем документе. Только после этого вся компания может переходить к следующей операции. Работа идет медленно, скрупулёзно, с обязательной громкой читкой, обязательным громким докладом об исполнении и распиской в особом технологическом журнале.
У нас таких строгих формальностей не было. Когда Шабаров обо всей этой методике рассказал Королёву, тот решил, что там, где мы будем работать вместе, надо «им показать, что мы не хуже». Ну, а что касалось нашей собственной деятельности, то для ракеты Р-5М необходимо было пересмотреть все инструкции по подготовке на технической и стартовой позициях и тоже ввести тройной контроль: основной исполнитель — воинская часть (офицер или солдат), контролирует офицер — специалист соответствующего управления полигона и обязательно представитель промышленности.
Так что и раньше в принципе можно было резко снизить брак и глюки в критически важных местах, но видно же, какое это мучение, как это долго и экономически невыгодно. Нужна некая золотая середина.
Другое дело — что если, как worldmind пишет, удастся сделать технические средства для устранения багов в коде и железе математическим путём и, разработав эту систему 1 раз, дальше можно будет использовать без затрат — это было бы неплохо.
vics001
17.12.2016 22:01Потому что земляне сами глючные, у кого-то криворукость, у кого-то дальнозоркость, кто-то быстро пишет код, но мало проверяет… Эволюция — выживают сильнейшие. И программы такие же выживают сильнешие, но глючат все…
Глючность это преимущество.
Lertmind
17.12.2016 22:54Эволюция — выживают сильнейшие.
Известное заблуждение: на самом деле суть в размножении. Биология поведения человека. Лекция #2. Эволюция поведения, I [Роберт Сапольски, 2010. Стэнфорд].vics001
18.12.2016 03:23«Эволюция — выживают сильнейшие», это крылатое выражение в данном контексте к тому, что останутся наиболее стабильные и полезные программы. А в биологии это значит, выживают (остаются) сильнейшие (наиболее полезные) признаки.
killik
18.12.2016 07:00+2Вовсе нет. В биологии это означает "выживают выжившие", то есть приспособленные. Сильнейшие признаки? Саблезубые тигры имели большие проблемы с позвоночником, и так по всему комбинату. А мыши пережили динозавров. В чем сила?
worldmind
17.12.2016 22:56Глючность нужна при эволюции, а те программы о которых речь не эволюционируют (не размножаются и не подлежат отбору)
vics001
18.12.2016 03:20Глючность — мутации. Суть в том, что неизвестно какое качество полезно, пусть появляются. Главный вопрос — «почему земляне делают глючный софт и железо», ответ — потому что сами такие.
Лучше написать глючную, но полезную программу, чем написать хорошую бесполезную. В принципе и бизнес так думает.
Было бы кому-то нужно написали бы идеальные программы. В математике (!), о которой идет речь строгих доказательств до 20 века не было. Эйлер суммировал расходящиеся ряды, Рамануджан большинство формул выводил методом приближений и иногда даже не доказывал, а уважаемый Ферма по всем решениям оставлял заметки на полях, с одной, правда, задачей плохо получилось.
Не пытаюсь никого переспорить, математика не формализировалась, пока это не стало нужно. Сейчас программы работают относительно стабильно, а ошибки быстро исправляются, зачем формальные доказательства?
Eklykti
17.12.2016 22:13+9кто уверен что вирус не начнёт ядерную войну?
Ядерная война,
Ядерная война,
Кто мне расскажет, кто подскажет,
Скоро ли она?vkegdzoy
17.12.2016 22:37-1Станислав Евграфович Петров вроде говорил, что вероятность ошибки или попадания в руки террористов вопрос времени. Эксперта по этому вопросу лучше него вряд ли возможно найти.
coturnix19
18.12.2016 13:56+2Ядерная война определенно переоценена. Мощность всего ядерного арсенала сравнима с всего одним пусть сильным, но даже не рекордным супервулканом. Ну, а заражение радиацией конечно неприятно но не смертельно.
demimurych
18.12.2016 15:33хм. а что вы думаете по поводу заявлений о том, что текущего ядерного запаса хватит на то, чтобы уничтожить землю n колличество раз?
coturnix19
18.12.2016 17:52Ну, во-первых раньше их было больше — не сильно но в несколько раз, правда это ничего качественно не изменит. Думаю преувеличивают для красного словца… разве что таки заражение радиацией имеют ввиду, хотя в инете говорится что за ~80 лет ядерной эры человечество уже взорвало около пол-гигатонны ядерного материала (в основном в тестах) (примерно 15% из этого — царь-бомба) и это почти не заметно, то вряд ли то что осталось даст сильный эффект. Конечно если использовать их по-назначению — т.е. взрывать в больших мегаполисах, то цивилизация сильно пострадает, может даже скатится до уровня мэдмэкса/фоллаута (на земле хватает мест где это само собой случается, без какой-либо ядерной войны), но земле вряд ли что будет.
Собственно, уничтожить землю буквально, как в «лекксе», по моему невозможно в принципе — грав. энергия связи слишком большая, первая космическая скорость соответствует температуре в порядка сотни тысяч градусов. Т.е. ее сначала нужно расплавить и испарить, а потому уже она начнет убывать в космос.
vkegdzoy
18.12.2016 17:22-1Действительно, переоценка такая сильная. Ничтожная переоценка, вон я смотрю в Чернобыле, Фукусиме прекрасно живут люди, выращивают пищу себе в почве, а не собирают её в мешки, разводят скот, а не забивают тысячи голов скота. И это ничтожные Уран-238 и Торий-232, при ядерном взрыве загрязнение начинается Плутонием-239 и Ураном-235. Загуглите их активность, тысячекратно выше. Смертельную дозу в 1 зиверт можно набрать за минуты.
coturnix19
18.12.2016 17:56+1На месте взрыва хиросимской бомбы действительно живут люди, и не парятся особо.
vkegdzoy
18.12.2016 18:52Ну так бомба было неэффективной.
sumanai
19.12.2016 04:41+1Скорее наоборот, современные бомбы меньше загрязняют поверхность, так как захватчику нужно земли, пускай и через несколько лет, а не радиоактивная пустыня на ближайшие 40000 лет.
coturnix19
19.12.2016 06:22+1Вроде как наоборот, для ядерных бомб чем эффективней — тем меньше фоллаута на единицу мегатонн. Ведь их главная цель — поджечь и разрушить инфраструктуру.
Alkul
19.12.2016 08:48+1при ядерном взрыве загрязнение начинается Плутонием-239 и Ураном-235. Загуглите их активность, тысячекратно выше
Бред. При взрыве атомного боеприпаса (хоть уранового, хоть плутониевого) загрязнение обуславливается осколками деления исходного материала боеприпаса.
Сам по себе уран-235 практически не радиоактивен, его период полураспада составляет порядка 10^8 лет. Это красноречиво говорит о его активности. У плутония-293 период полураспада 24000 лет, активность повыше, конечно. Давайте попробуем прикинуть величину загрязнения, если предположить, что плутониевый заряд не взорвался, а просто равномерно распылился по территории вследствие взрыва обычного ВВ (аналог «грязной бомбы»). Считаем:
Дано: активность одного грамма плутония-239 — 2,3ГБк, масса боезаряда порядка 50 кг, распыление происходит на круг диаметром 5 км.
Пересчитаю активность из беккерелей в кюри, получу активность грамма плутония 62мКu, активность всего боезаряда — 3108Кu. Площадь круга радиусом 5 км составит 78,5 кв.км. На каждый квадратный метр при этом придется активность порядка 40 мкКu, или примерно 1,5МБк. Это много. Но зиверт за минуту не набрать.
Но, повторюсь, загрязнение после взрыва атомного боеприпаса осуществляется не исходным изотопом — он практически полностью распался, а осколками деления, которые действительно, очень радиоактивны на несколько порядков выше своих родительских изотопов.vkegdzoy
19.12.2016 22:39зиверт за минуту не набрать
Ну если посчитать и другие радионуклиды в центре взрыва, то можно и поспорить. В любом случае я хотел показать, что при ядерном взрыве заражение гораздо более серьёзное, чем при аварии на АЭС.Alkul
20.12.2016 06:11Давайте попробуем посчитать.
Дано — реактор ВВЭР-1000. Масса топлива в одном ТВЭл — 1,565 кг. В тепловыделяющей сборке (ТВС) 312 ТВЭл, в активной зоне 163 ТВС. Итого общая масса топлива в активной зоне составит 79589 кг. Так как обогащение топлива у ВВЭР-1000 составляет от 3,3 до 4,4 процента (возьмем в среднем за 4 процента), то масса чистого U-235 составит 3183 кг. Предположим, что выгорание составило 50%, то есть, распалась половина массы U-235 — все атомы в 1590 кг урана распались на осколки (крайне радиоактивные, как я уже говорил).
Теперь сравниваем это массу радиоактивных веществ с массой радиоактивных веществ, образовавшихся при делении всех атомов U-235 в 100 кг атомного боеприпаса.
Итак, при тепловом (неатомном) взрыве на АЭС и произошедшем вследствие этого распределении топлива по территории загрязнение в 15 раз превысит аналогичное загрязнение от взрыва атомного боеприпаса.
Конечно, это некорректное сравнение в плане того. что мы не учитываем другие поражающие факторы атомного взрыва — ЭМИ, нейтронный поток, световое излучение, ударная волна. Плюс, естественно, при атомном взрыве радиоактивные вещества будут разбросаны на бОльшее расстояние, чем при тепловом взрыве на АЭС. По совокупности поражающих факторов ущерб от атомного взрыва, скорее всего, будет превосходить ущерб от теплового взрыва на АЭС.
Но если говорить только о загрязнении, то в последнем случае загрязнение будет значительно выше (чисто по массе РВ — в 15 раз), плюс распределится это загрязнение на меньшую площадь, а значит, удельное загрязнение на единицу площади будет еще больше.
Alkul
20.12.2016 06:18И это, кстати, мы посчитали только по топливу, без учета массы конструкций активной зоны, которые вследствие постоянного облучения нейтронами приобрели наведенную радиоактивность, а значит, тоже будут давать вклад в загрязнение.
Alexeyslav
20.12.2016 14:06Наведённая активность быстро сходит на нет. Это если в структуру материала внедрились атома радиоактивного вещества — только тогда будет проблема. Но это по большей части лишь поверхностное загрязнение.
Alkul
20.12.2016 17:35+1Вы не правы. Наведенная активность главным образом обусловлена облучением материала потоком нейтронов. Атом стабильного изотопа может захватить нейтрон и превратиться в нестабильный (т.е., радиоактивный) изотоп. А как быстро наведенная активность «сойдет на нет» — будет зависеть только от вида полученных изотопов, в зависимости от их периода полураспада.
Погуглите, что такое «наведенная активность», если не верите мне.Alexeyslav
20.12.2016 17:57Только вот если материал не урановый лом, долгоживущих изотопов не выходит. Основная проблема загрязнения материалов — это поверхностная активность, хуже конечно когда железка 30 лет работала в реакторе — тогда да, будет долго «остывать» ещё и за счёт диффузии изотопов топлива в материал.
Alkul
20.12.2016 18:09+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 лет. Тоже немало на самом деле.
fenrirgray
17.12.2016 22:13+2Есть такой метод/подход к написанию программ, называется formal verification(формальное доказательство) и вытекающее из него «доказательное программирование». Так что идея ваша совсем не нова, она была довольно популярна в академ кругах в 70-х, 80-х годах.
Идея не пережила коммерциализацию, в связи с крайне высоким уровнем сложности реализации для сколько-то сложных программ. На данный момент впрочем, в связи с ростом связности систем, интерес к концепции по немногу возрождается.worldmind
18.12.2016 12:48Именно об этом подходе моя статья
5oclock
19.12.2016 12:34+1А вот можно «на пальцах», так сказать, рассказать как технически может выглядеть построение программного обеспечения системы, например, управления поездами на станции?
Просто статьи про функционально безопасное ПО зачастую очень общи, содержат пространные рассуждения, много воды. И эта статья не исключение.
А вот если приземлённо, без теоретизирования: объясните программистам пишущим софт для управления железнодорожной станцией — как они должны его писать?
Чтобы рассуждения не были опять-таки отвлеченными, пусть структура системы будет такой:
1. Т.н. напольное оборудование (стрелки, сигналы, рельсовые цепи, ну и всякое по-мелочи).
2. Шкаф управления напольным оборудованием обеспечивает безопасную увязку с п.1. Функционально безопасную. Т.е. объекты будут изменять состояние только по командам и никак не самопроизвольно, сигнализация от объектов будет поступать корректная, однозначно соответствующая их реальному состоянию. Это, вообще говоря, тоже не тривиальная задача.
3. Центральный Вычислительный Комплекс (ЦВК).
4. АРМ пользователя. Собственно он не обязан быть безопасным. Вся безопасность заключается в ЦВК.
ЦВК это, к примеру, трёхканальная система, работающая по мажоритарному принципу (2-из-3). Если один канал начинает выдавать данные, не совпадающие с остальными двумя — он отключается и система начинает «хромать» по принципу 2-из-2: ЦВК управляет только пока выходные данные обоих оставшихся комплектов совпадают. Возможно с урезанием функционала.
Если же начинают расходиться данные оставшихся комплектов — система переходит в защитное состояние до вмешательства обслуживающего персонала.
Чисто алгоритмически, ЦВК выполняет увязку стрелок, сигналов и рельсовых цепей так, чтобы не допустить враждебностей и опасных воздействий на подвижной состав (перевод стрелки под составом, некорректное перекрытие сигнала перед поездом).
Ну и, понятно, нужно обеспечить пропуск поездов по станции с требуемой интенсивностью.
Как к данной задаче применить упомянутый Вами метод создания ПО?worldmind
19.12.2016 14:08Писать-то можно также, а вот проверять по другому — математически доказывая, что программа делает, то, что описано в требованиях, я приводил ссылку на доказанное микроядро — у них вроде опубликована научная работа о том как они это делали.
Без теоретизирования математическую теорию никак не объяснить, но тут в комментах говорят о знакомстве с теми, кто занимается формальной верификации, можете попробовать напросится на лекцию.5oclock
19.12.2016 16:40Писать-то можно также, а вот проверять по другому
Как же «также»?worldmind
19.12.2016 17:00В соответствии с методологиями применяемыми в таких сферах, обычно в таких компаниях процесс налажен и/или есть внешние требования от сертифицирующей организации, у меня вопрос вызывает ассоциации с Pmbok и т.п.
5oclock
19.12.2016 18:12Ладно.
И как доказать, что в программе нет зависимости состояния сигнала в одной горловине от положения стрелки — в другой? Кроме нормативного конечно.
Полным перебором всех комбинаций всех значений всех сигналов и переменных со всеми временнЫми выдержками? (время — это тоже параметр)worldmind
19.12.2016 18:28Изучить теорию доказательства программ и доказать. Вроде даже есть общедоступные онлайн курсы.
5oclock
19.12.2016 18:45+2Я не пойму, Вы распинаетесь с этой идеей уже второй день и не хотите на предложенном примере проиллюстрировать её преимущества или хотя бы работоспособность?
zzzcpan
19.12.2016 19:23+1Почитайте вводные статьи по TLA+/TLC/TLAPS, как раз из вашей области. Вот пример на TLA+, для проверки подобного отсутствия зависимостей, правда для снэпшотов.
shulyakovskiy
17.12.2016 22:18Современный персональный компьютер (ПК) — это всего лишь баловство, которое может помочь человеку самовыражаться. Через это самовыражение и происходит развитие, как человека, так и ПК. Человек балуется с ПК, а баги на ПК балуются с человеком, все тут сходится.
Другое дело, если говорить о микропрограммах для жизненно важного оборудования, вот там да, стоимость бага сильно велика и конечно этому стоило бы уделять побольше внимания, возможно даже и на мировом уровне, вот только, что делать с «загребущими руками»? Если начинать вливать в эту отрасли большие деньги на зарплату, то сразу найдутся люди, которые просто будут нахлебниками и средний интеллект в такой команде не увеличится. Да, через пару тройку лет возможно и получится отсеять некоторых недобросовестных людей, но за это время добросовестные задолбутся получать по шапке за тех, кто криво делает. Наказания спросите вы? А что стоит наказания одного раздолбая, если выпущеный серийный аппарат МРТ, например, поджарит пару десятков человек?
Ну дальше я не буду развивать эту тему, наверно стало немного понятно, что хорошее оборудование с малой вероятностью появления багов стоит очень дорого и не из-за того, что там работают дорогостоящие сотрудники и загребают деньги лопатой, а из-за того, что весь этот процесс очень и очень сложно организовать из-за человеческой натуры.
Ровно из-за этого на наше с вами баловство с ПК ни кто не будет писать софт без багов.Hellsy22
17.12.2016 22:22+3если выпущеный серийный аппарат МРТ, например, поджарит пару десятков человек
Серийно выпускаемые автомобили убивают около 3500 человек в мире каждый день. Многим это не нравится, но от автомобилей никто избавляться не спешит.shulyakovskiy
17.12.2016 22:25Я и не говорил, что от них надо избавляться. Более того, автомобили — поповозки — это в большинстве случаев тоже баловство и покупая себе автомобиль, человек берёт на себя ответственность в том числе и за его баги, Если они конечно не сильно явные и их можно интерпретировать, как особенность.
Hellsy22
17.12.2016 22:31Я к тому, что смерть двадцати человек — это, конечно, не слишком хорошо, но люди умирают все время и потому важен баланс. Если из-за ожидания нового медицинского устройства погибнут 200 или 2000 человек, то риск, как мне кажется, оправдан. Я лишь хотел бы быть информированным о подобных рисках.
worldmind
17.12.2016 22:23Никуда вливать ничего не нужно, нужно чтобы аппарат МРТ не проходил сертификацию, не допускался к эксплуатации если его прошивка не верифицирована.
shulyakovskiy
17.12.2016 22:29+1Вот это будет очень большой проблемой в развитии любой отрасли. Если так сделать, то возможно останется одна фирма, которая сможет пройти сертификацию верифицировав весь свой код. Но стоимость будет заоблачной, Позволить себе это смогут только отдельные клиники, стоимость лечения в которых будет тоже очень высокой. Большенство людей останется без диагностики.
Эту проблему надо решать по другому. А вот небольшой наброс на вентилятор: представь теперь, что писать код для него будет тот человек, которому этот аппарат необходим, какова вероятность того, что он халатно отнесётся к написанию программы?worldmind
17.12.2016 22:34Заоблачной стоимость будет только если каждый производитель каждый раз будет заново писать и верифицировать весь свой код, а если будут использованы ранее верифицированные открытые компоненты, то стоимость вырастет не сильно.
А неважно насколько халатно человек отнесётся, человек при всём своём желании не может быть безошибочным, одни когнитивные искажения чего стоят, а есть куча других факторов (не доспал, простыл, отвлекли, не сообразил, забыл...) из-за которых даже самый ответственный человек может ошибиться.
Человек не надёжное звено в любом случае, каким бы он ни был.shulyakovskiy
17.12.2016 22:40И вот тут мы подошли к самой главной теме, которая не раскрыта в этой статье «Стоимость и временные затраты на написание верифицированного кода»
worldmind
17.12.2016 22:51отсюда: «Для проведения теста было взято микроядро Secure Embedded L4 (seL4), содержащее 8700 строк кода базирующегося на open source проекте OKL4…
Работой по формулировке алгоритма математического доказательства в течение четырех лет занималась команда из 12 исследователей NICTA, аспирантов и техников. Они успешно проверили более 10 тыс. промежуточных теорем, изучив более чем 200 тыс. строк кода. Итоговый анализ выполняется с помощью интерактивной программы Isabelle, и на сегодняшний день является самой объемной автоматизированной проверкой выполнения условий теорем.
Наряду с доказательством соответствия программного кода выполняемым функциям, тестирование показало, что seL4 не подвержен большинству известных хакерских атак. Например, атака «переполнение буфера», позволяющая внедрить злонамеренный код и захватить управление работой ядром, не даст результата.»
Примерно миллион долларов и человечество получило микроядро беспрецедентной надёжности, доступное всем по свободной лицензии.shulyakovskiy
17.12.2016 23:19И 4 года на проверку, заметь не написание, а только на проверку. Плюс мне кажется, что уязвимости и проблемы в бизнес логике имеют несколько разный характер появления.
Уязвимости да действительно появляются из-за человеческой невнимательности. А вот проблемы в бизнес логике, чаще появляются из-за проблема коммуникации между людьми. Программист их намеренно делает думая, что так и надо.
Тут же возникает вопрос о специалистах которые хорошо шарят не только в программировании но и в области той науки для которой он пишет софт, а это очень часто редкие люди. возможно стоит пойти дальше и пересмотреть подготовку специалистов, убив еще 2-3 десятка лет.
В любом случае верификация кода на очень быстро развивающихся железках (я не говорю о баловстве с ПК) — это очень проблематично.worldmind
17.12.2016 23:321. 4 года для 12 человек, возможно это параллелится (раз работал не один, а 12, то вероятно это так), это не так много за такой уровень надёжности. Если бы это было международным проектом, то уже был бы верифицированный весь стек технологий для разработки.
2. Проблема с корректностью требований не решается верификацией, это я отметил, но с требованиями проблемы в бизнесе, а в медицине, авиации, космосе, АЭС требования вынуждены формулировать максимально точно (иначе оно бы и не работало).
3. Да, специалисты нужны другого уровня, не обезъянокодеры, а математики-программисты. Да, нужно начинать их готовить, если этого не делать, то так и будем терять космические аппараты с бешеной стоимостью из-за программных ошибок, проводить некорректные исследования из-за багов в МРТ и т.п.xhumanoid
18.12.2016 09:33Анонс свежего ядра 4.8:
>> В новую версию принято более 13 тысяч исправлений от примерно 1500 разработчиков, размер патча — 41 Мб (изменения затронули 11303 файлов, добавлено 627751 строк кода, удалено 278958 строк).
вопрос: сколько людей и сколько времени будет проходить верификация только нового кода?
8700 строк кода — 12 человек — 4 года
348793 новых строк кода — ? человек — ? лет
дополнительно учитываем, что сложность верификации совсем нелинейна относительно объема кода (лично я допускаю что ближе к экспоненте)
Да, многие вещи в ядре дублируются и тд, тех же fs вагон и маленькая тележка, но все они кому-то нужны, так как специализированны под конкретные требования, нельзя написать одну fs которая удовлетворит всех, а потом её верифицировать и все счастливые.
p.s. сам регулярно прогоняю статический анализ по своему код, но это далеко не верификация, так как она будет не просто дорого, а очень дорого, проще переписать 10 раз с нуля под изменившиеся требования, чем 10 лет пилить морально устаревшее решениеworldmind
18.12.2016 10:22Монолитное ядро пока нет шансов верифицировать, да и не нужно, а вроде старался это отметить — первоочередная задача это верифицированное микроядро для встраиваемых систем, и к счастью оно уже есть, можно двигаться дальше.
xhumanoid
18.12.2016 10:39вот тут подходим к другому пункту:
верифицированный L4 это по сути минимальный гипервизор, который почти ничего не умеет.
В самом linux kernel от ядра как таковое совсем малый процент
первое место по объему это драйвера
дальше уже arch (все-таки количество поддерживаемых архитектур зашкаливает, сравните с seL4 который 4 вида arm и одни ia32 тянет)
и третье место за fs.
то есть формализовать только какой-то subset от ядра не проблема даже для монолита.
а вот формализовать все ядро действительно нету шансов
к тому же если посмотрите на последние уязвимости-ошибки, то окажется что по отдельности они не несут никаких деструктивных вещей, зачастую это даже ожидаемое их поведение, но вот грамотное построение цепочек из 10-15 таких недоуязвимостей создают большую дыру и тут даже верификация и микроядро не поможет, так как каждое из действий будет считаться допустимым, а истинная проблема возникнет на стыковке и объединении всех модулейworldmind
18.12.2016 10:47По идее именно гипервизор, да несколько драйверов нужно верифицировать для конкретной архитектуры и писать на чём-то вроде си, а всё остальное на условном кроссплатформенном хаскеле нужно писать (и его компилятор верифицировать для архитектуры) и его верифицировать будет проще благодаря математичности языка.
Но конечно в сфере о которой я говорю не будет такого зоопарка архитектур, ФС или устройств.xhumanoid
18.12.2016 11:11+1«Блажен, кто верует, тепло ему на свете!»
и вот тут мы начинаем спускаться уже глубже:
ядро для os для атомных, космических и медицинских вещей и так далеко не обычное используется, говорить, что там меньше архитектур и fs я бы точно не стал, так как хватает всего, поэтому и разработки такие дорогие, что продукты очень часто близки к уникальным или тираж очень маленький.
«а всё остальное на условном кроссплатформенном хаскеле нужно писать» — все любят повторять это как мантру, раз математический язык, то все хорошо, но почему-то все забывают уточнять, что как только поменялась немного модель данных, то с хаскелем все очень весело становится, про разворачивание ошибок компиляции отдельный вопрос (это все вытекает из математики).
иногда проще поступить по принципу эрланга: если что-то падает, дай ему упасть.
Но в нашем случае продолжаем работать и принимать решения уже на оставшихся данных, так как любая физическая сущность всегда может упасть или начать возвращать неправильные данные (можете посмотреть количество сбоев обычной RAM в датацентрах, интересная статистика, посмотрите на последние уязвимости Rowhammer), то есть ваша программа формально будет вести себя правильно, но данные ей будут поступать некорректные.worldmind
18.12.2016 12:05> говорить, что там меньше архитектур и fs я бы точно не стал
но не факт, что это потому что так необходимо, скорее всего можно свести к паре-тройке вариантов
evpevp
19.12.2016 08:32Мне кажется, что кто-то не хочет понимать прочитанное, а кто-то не понимает смысла даже своего сообщения. Обратите оба внимание на то, что двенадцать человек четыре года занимались «работой по формулировке алгоритма математического доказательства». Они провели огромную работу за это время. Плодом этой работы стала «интерактивная программа Isabelle». И вот уже с помощью нее был проведен анализ микроядра. Сколько труда ушло на анализ не уточняется. Но не четыре года :) Думаю, порядка дня-двух, а может и меньше.
arheops
17.12.2016 23:23+1… но не факт, что в работе этого микроядра нет багов. Поскольку еще есть компилятор и железо.
worldmind
17.12.2016 23:33конечно, это всего лишь пример одного из кирпичиков в фундаменте надёжного ПО будущего
arheops
17.12.2016 23:44+1Угу, только на верификацию новой модели процессора будет потрачено 50 лет(там еще физ эффекты же есть, не только логика), а верифицированный компилятор будет компилировать неделями hello word.
worldmind
17.12.2016 23:48Где-то мелькала инфа что с процессорами как раз проще (во всяком случае со схемой).
А есть что почитать про медленно компилирующий верифицированный компилятор?arheops
17.12.2016 23:56+1Верифицированные вещи вообще медленные. Потому, что в некоторых случаях(в очень большом проценте) проще убрать оптимизацию, чем ее верифицировать. Например, развертки циклов и так далее. Просто вам прийдется сделать компилятор очень минимальным, убрать все оптимизации и каждую следующую версию ждать десятилетия.
Верифицировать схему не особо сложно. Сложно верифицировать ситуацию «в этом куске кремния нет неучтенных эффектов». Вам же его и производить прийдется на верифицированном оборудовании. Сейчас при запуске очередного техпроцесса уходят месяцы подтасовок оборудования(называемых «наладка техпроцесса»), в случае верификации вы должны ее заново начинать после любого минимального изменения неучтенного в предыдущих теоремах.worldmind
18.12.2016 09:42Кусок кремния сейчас это самое надёжное звено в цепочке кремний-схема-софт, поэтому возможно начать нужно со схемы и софта
worldmind
18.12.2016 09:55+1> проще убрать оптимизацию, чем ее верифицировать
компилятор тогда быстрее будет — не будет заниматься оптимизациейarheops
18.12.2016 10:01Ем? Вам же прийдется убрать и оптимизации по скорости. У вас какие-то странные представления о том, как устроены компиляторы и системы доказательства теорем.
sumanai
18.12.2016 00:05Скорее даже не столько компиляция будет медленной, сколько скомпилированная таким компилятором программа будет медленной.
arheops
18.12.2016 10:02Компиляция тоже будет не быстрой, поверьте. Во всяком случае компиляция чего-нибудь современного(с библиотеками в тысячах файлов и десятками тысяч заголовочных файлов).
Priapus
18.12.2016 14:13Произведем грубый расчет.
Считается, что квалифицированный программист может выдавать 200 строк качественного, оттестированного кода в день. Таким образом, 8700 строк было бы написано 1 программистом за, примерно, 2 месяца (с учетом выходных).
Получается, что потрачено 2 человеко-месяца на разработку и 576 человеко-месяцев на тестирование.
На этом дискуссию можно заканчивать. Такое делается 1 раз с целью показать: «вот, смотрите, как мы можем», — но в реальной жизни это неприменимо. Хотя бы потому, что не существует необходимого количества «исследователей».Idot
19.12.2016 14:27+2квалифицированный программист может выдавать 200 строк качественного, оттестированного кода в день
Хрень полнейшая! Вы — индийский менеджер на индусскими программистами?
Всё зависит от задачи — можно, и две строчки за весь день выдать, если ищешь ошибку среди десятка тысяч строк, а можно и две тысячи строк за день накатать, если задача простая и ясная.Priapus
19.12.2016 14:33Вы точно программист? Речь о среднем значении. Понаберут по объявлениям…
И я посмотрю как вы 2000 качественного оттестированного кода в день сделаете без копипасты и искусственного набивания статов. Сказочники.
Ааа, все понятно. Уходи.
herr_kaizer
18.12.2016 09:29А потом мы слышим нытье «ой, а чего это лекарства такие дорогие».
worldmind
18.12.2016 10:20Дорогие они скорее по другим причинам.
Конечно это не удешевляет медицину, но повышает надёжность, куму нужна ненадёжная медицина?xhumanoid
18.12.2016 11:19+1использовать ненадежный МРТ сейчас за цену Х
или его появление в 10 клиниках в мире через 20 лет за цену 1000*X
я выбираю первый вариант, так как в некоторых случаях это нужно здесь и сейчас, а не через год, не говоря уже о больших сроках. многие новые разработки являются уникальными, либо используют новые физ-мат модели и переиспользовать просто нечего, поэтому фраза оказывается ложной:
>> Заоблачной стоимость будет только если каждый производитель каждый раз будет заново писать и верифицировать весь свой код, а если будут использованы ранее верифицированные открытые компоненты, то стоимость вырастет не сильно.
даже с обычной жизни мы постоянно сталкиваемся с вероятностями в медицине:
экспресс тесты на беременность/ВИЧ/диабет.worldmind
18.12.2016 12:10> ненадежный МРТ сейчас за цену Х или его появление в 10 клиниках в мире через 20 лет за цену 1000*X
Не будет такого выбора.
Речь не о том, чтобы остановится в развитии, а о том, что надо двигаться в правильном направлении, вот есть у нас теперь верифицированное микроядро, значит стоит использовать его в новых МРТ, а не костылить что-то своё, появится следующий верифицированный компонент (например ФС), значит новое нужно делать используя его.Priapus
18.12.2016 13:24Не будет такого выбора.
Речь не о том, чтобы остановится в развитии, а о том, что надо двигаться в правильном направлении, вот есть у нас теперь верифицированное микроядро, значит стоит использовать его в новых МРТ, а не костылить что-то своё, появится следующий верифицированный компонент (например ФС), значит новое нужно делать используя его.
Вы уже 10 раз это написали. Дайте пруф, что это так. И с чего вы взяли, что я, потратив очередные 48 человеко-лет на верификацию своего компонента (например ФС), разрешу вам использовать его бесплатно? Цена в 1000*Х это, на мой взгляд, даже оптимистичный прогноз.worldmind
18.12.2016 13:41Пруф в статье — ссылка на верифицированное микроядро под gpl.
Это конечно один пример, но тут ситуация как с линуксом — каждому в одиночку такое пилить слишком дорого, поэтому компании-конкуренты скидываются и пилят ядро вместе, а защитой для них является GPL.Priapus
18.12.2016 14:03+1Где в статье пруф, что не будет удорожания разработки и увеличения сроков? В статье как раз пруф того, что на несчастные 8700 строк кода потратили 48 человеко-лет и это не дает никаких гарантий отсутствия программных ошибок.
Это конечно один пример
Это пример того, как по приколу напряглись и показали как подход можно применить для микроштуки, угробив, как минимум, в 50 раз больше ресурсов, чем требовалось.
Дайте расчет или пример того, сколько придется угробить ресурсов для десятка миллионов строк кода. Только не надо сказок про то, что мы сделает 100500 финтифлюшек, протестируем каждую и это будет гарантировать, что все вместе они заработают как надо. Не позорьтесь.worldmind
18.12.2016 14:27> Где в статье пруф, что не будет удорожания разработки и увеличения сроков?
Я вроде пояснил уже, что если верифицированные компоненты будут создаваться не в рамках конкретных продуктов, а параллельно, то они не будут замедлять их развитие, и не сильно будут увеличивать стоимость т.к. затраты будут распределяться по большому количеству продуктов в которых они используются.
Так, например, весьма большая стоимость свободных дистрибутивов не приводит к дороговизне домашних роутеров построенных на них.Alkul
20.12.2016 17:56+2Вы раньше писали, что Вы не специалист в этой теме. По-моему, на этом можно и поставить точку в дискуссии.
svboobnov
17.12.2016 23:18Господа, а давайте-ка вспомним, что многие из нас называются «инженерами-программистами» или «software engineers».
А ещё вспомним, что раньше, в 19 веке, среди инженеров — мостостроителей, было принято становиться на лодке под построенным мостом, когда по нему пускали первую нагрузку (поезда, телеги).
Так вот, ежели заставить разработчиков софта для МРТ и авионики на себе испытывать эти установки, ответственность сама по себе возрастёт (никто не захочет умереть от своего изделия).
То есть, банально восстановим принцип персональной ответственности инженеров за свои изделия.
ClearAirTurbulence
18.12.2016 02:03С МРТ нудачный пример, он не может поджарить физически.
a5b
18.12.2016 02:29+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."a5b
18.12.2016 05:15+1http://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, при котором выкипает жидкий гелий)
coturnix19
18.12.2016 04:12А что стоит наказания одного раздолбая, если выпущеный серийный аппарат МРТ, например, поджарит пару десятков человек?
Такое уже было, мне известен как минимум один прецедент (правда не мрт конкретно, но суть та же)
user343
20.12.2016 01:48При УЗИ беременных сканер Тошиба 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) анекдот: "С тех пор, как я начал водить машину, я стал осторожнее переходить дорогу."
Hellsy22
17.12.2016 22:20+1Думаю, для того чтобы земная цивилизация устойчиво развивалась
Думаю, что прежде, чем вносить какие-то предложения по устойчивому развитию, было бы неплохо обосновать смысл и пользу именно устойчивого развития по сравнению с альтернативами. А то этот термин стал нарицательным и вобрал в себя всю палитру оттенков ретроградства, бессмысленной перестраховки и, как итог, тотальной неэффективности.worldmind
17.12.2016 22:26В данном случае речь о защите от техногенных катастроф связанных с ошибками в ПО.
Hellsy22
18.12.2016 06:25Вероятно, защита должна быть принципиально иной — направленной на минимизацию возможного ущерба, а не на надежду полностью его избежать. Т.е. дробление опасных производств, замена по возможности на безопасные аналоги, вынос их как можно дальше из городской черты и т.д.
worldmind
18.12.2016 10:17поясните что имеете ввиду на примере разработки ПО для космических аппаратов, кого дробить и выносить?
sumanai
18.12.2016 17:48разработки ПО для космических аппаратов
о защите от техногенных катастроф
Так аппараты или катастрофы? Упавшая ракета разве что дом какой может поломать.worldmind
18.12.2016 18:03И то и то конечно, параллельно несколько веток потерял нить. Касательно техногенных катастроф, можно представить например ситуацию когда интернет стал основополагающей инфраструктурой цивилизации — ничего без него не работает, врачи не могут оперировать (не каждого пациента привезёшь к нужному хирургу), экономика не работает — ничего нельзя купить без сети (без доступа к блокчену или банку), образование не образовывается т.к. ехать за тридевять земель к нужным преподавателям никто не хочет, да и сами преподаватели частино живут не пойми где и т.д.
Можно конечно вернуться в каменный век для надёжности, а можно сделать технологии лежащие в основе интернета столь надёжными чтобы никакие хакеры не могли остановить жизнь цивилизации.xhumanoid
18.12.2016 20:20Написали мы софт, верифицировали, а потом
1) трактористы Васи порвали экскаватором оптику (реальный случай пропадания аплинка между РБ и Россией, в тот момент там свыше 50% всего внешнего канала было, сколько рвут кабелей океанических вообще помолчим).
2) ударили молнии и вторая половина датацентров легла (случай с амазоном)
Распределенные технологии, такие как интернет, по определению строятся на ненадежных системах, чем больше узлов в системе тем выше вероятность отказа. Поэтому для интернета стоит задача другая: как из ненадежных элементов построить достаточно устойчивую систему. Отмирание отдельной клетки не убивает организм (рак отдельная песня, но и с ним частично борются), выпадение одного сервера не ложит yandex/google/facebook (для них вылеты целиком стоек никак не сказываются на работе, даже падение целого датацентра не остановит работу). Те же DDoS это полностью правильная работа, но датацентр можно положить, тут не спасет никакая верификация.
Поэтому отдельные части верифицировать можно, но чем крупнее система, тем больше нужно полагаться на общую устойчивость, а не на то, что у нас каждый элемент будет работать правильно и идеально и никогда не сбоить.worldmind
18.12.2016 20:27Речь не о защите от отмирания одной клетки, а скорее об устойчивости к вирусу могущему поразить все или значительное количество клеток.
xhumanoid
18.12.2016 20:43+1и верификация с математикой нам тут ничем не помогут, так как они не спасают от аппаратных сбоев, они не спасают от направленной атаки (Rowhammer уже приводил), они не спасают от направленного внедрения (когда человек сам запускает тот же вирус или он оказывается установленным еще на заводе изготовителе).
Shubinpavel уже вам ответил за космос: проблема зачастую в ресурсах (время, деньги, человеки) когда сознательно идут на срезание улов и уход от поставленных требований к проверке надежности, но чтобы было хоть что-то, а не воздушные замки в мечтах.
NASA имеет бюджет, любой спутник или ракета имеет бюджет, поэтому иногда возможно рискнуть и попытаться запустить сейчас с вероятностью неудачи в 0.001% чем пропустить запуск и ждать следующих 4-5 лет для появления окна запуска. В случае неудачи у вас есть риск строить такой же аппарат еще 8 лет, но это сознательный риск.
Не задумывались почему даже на Curiosity обновление прошивки заливали уже после достижения Марса: в момент отправки оно просто не было готово, не хватает ресурсов.
zzzcpan
18.12.2016 20:34+1Так эта «общая устойчивость» — тоже алгоритмы и их тоже можно верифицировать. Точнее даже в распределенных системах только их в первую очередь и имеет смысл верифицировать, сам Лесли Лампорт главный адвокат такого подхода с его TLA+.
xhumanoid
18.12.2016 20:44Вот, мы верифицируем общую устойчивость и я с этим полностью согласен и пытаюсь это донести.
Верифицировать и гарантировать работу ВСЕХ составляющих дорого, долго и не имеет смысла.
Delics
17.12.2016 23:37Почему земляне делают глючный софт и железо
Прежде всего потому, что заказчики (или покупатели) мирятся с глюченностью и недоделанностью софта или схем.
надо иметь математическое доказательство этого утверждения
Вообще-то надо просто проверить, как работает. В разных ситуациях и с разными данными.
Математическое обоснование тут не подходит, т.к. задача слишком сложная и нелинейная. Строгого решения вы просто не найдете.Alexeyslav
19.12.2016 16:15+1И сразу же сроки проверки простейщей программы стремятся к бесконечности! Это как проверить устойчивость алгоритма хеширования на предмет коллизий. Всего каких-то 256 бит, и времени всей вселенной на нынешних скоростях не хватит чтобы проверить все варианты. Тут как раз математическое обоснование выглядит гораздо более простым и реализуемым.
Простейшая, даже самая очевидная программа — X = A + B где A и B — целые 32-битные числа. Количество вариантов которое надо проверить чтобы выдать положительный вердикт — 2^64 степени, при вычислительной мощности процессора 1000МFLOPS время на тест такой простейшей программы полным перебором составит не менее 18446744073 секунд, или почти 585 лет непрерывной работы. И это для простейшей очевидной программы, работоспособность которой легко доказать.
den_golub
18.12.2016 00:36+1Да, соглашусь 2 и 3 проблемы, можно скорее всего закрыть предложенным способом. А как насчет первого? Идеальной защиты от дурака не напишешь. Люди в свое глупости(ну или лени) очень изобретательны.
И по-моему Вы упускаете один аспект или как вы их называете причину, как насчет того что человек в силу своей несовершенности не может учесть всего? Взять ту же АЭС, сможете перечислить все возможные варианты событий, которые могут произойти и которые надо учесть в ПО? Мы в обычной жизни не всегда можем все варианты просчитать, что уж говорить о сколько-нибудь серьезных проектах. И тут уже проблема не в глючности, а именно в том что все это для начала учесть, а потом и запрограммировать, а потом еще и проверить.worldmind
18.12.2016 09:55Да, я отмечал, что проблему корректно сформулированных требований это не решает, но во-первых, это не отменяет нужности верификации, во-вторых, в проектах критического уровня требования всё же стремятся сделать (благодаря этому АЭС работают, самолёты летают) и самое главное — если мы вдруг обнаружили ошибку в требованиях и исправили и верифицировали, мы точно знаем, что улучшили систему, уверены что исправляя не внесли новых багов т.е. мы поднимается по лестнице развития, а колеблемся около горизонтальной оси исправляя одно и ломая другое.
5oclock
18.12.2016 11:05А как проверять тех кто проверяет?
worldmind
18.12.2016 12:04А как с сейчас проверяют? Речь же не о волшебной палочке, а об улучшении одной составляющей процесса (проверки программ), остальные остаются теми же.
5oclock
18.12.2016 23:10Ну т.е. Вы переносите ответственность за корректность программы на какой-то другой уровень.
А корректность самих «проверяльщиков» (будь то ПО или люди) как проверить?
Почему проверенная ими программа будет более корректной если мы не можем доверять проверяльщикам?worldmind
19.12.2016 08:30Да никак нельзя проверить проверяльщиков, это будет бесконечная цепочка проверки, поэтому на практике ограничиваются двумя звеньями — одни делают, другие проверяют
azsx
18.12.2016 03:46-1Скажите, а может более оптимален такой вариант? Дублировать программы от разных программистов?
Допустим, надо вычислить высоту над поверхностью. Расчёт высоты ведётся не одной подпрограммой, а тремя одновременно, но три подпрограммы разные по алгоритму и писались разными программистами. Если объёмы устройств позволяют, то компьютеров физически три. Управляющее устройство срабатывает, если от двух и более алгоритмов поступили одинаковые цифры.Hellsy22
18.12.2016 06:27А если не поступили, то летательный аппарат, стало быть, теряет управление и зависает в воздухе, ожидая сервисной команды?
dipsy
18.12.2016 08:00Вариант хороший, но в 3 раза дороже, чем обычные решения. Для военки и космоса наверное подойдет. С другой стороны для достаточно сложных случаев такой подход не сработает, грубо говоря облететь препятствие можно и правильно слева или справа, сверху или снизу, будет ситуация как в той басне, все тянут в свою сторону и все правы.
worldmind
18.12.2016 10:09Так иногда и делают в критичный областях типа авиации и космоса, но даже это не всегда помогает
worker
18.12.2016 19:47так было на Шатле 4 одинаковых компьютера и 1 совершенно другой от другой компании
и тоже был какой-то инцидент
Alexx999
18.12.2016 05:00Интересно одно — с точки зрения современной математики это реализуемо? Как минимум у машины Тьюринга есть проблема останова неразрешимость которой вполне себе доказана, так что тут есть фундаментальные ограничения. Было бы очень интересно узнать мнение эксперта в этой области.
worldmind
18.12.2016 10:11Судя по ссылкам на ядро L4 которые я привёл это не только реализуемо, но и реализовано.
Rulexec
18.12.2016 12:27+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, но и доказательство того, что у переданного значения вес меньше, чем у предыдущего. Тогда, очевидно, рекурсия не сможет продолжаться бесконечно, т.к. когда-нибудь она упрётся в нижнюю границу.
И все наши программы будут завершаться когда-нибудь (если никто не будет вычислять что-нибудь невероятно долгое, вроде функций Аккермана — ограничивать по времени выполнения куда сложнее, придётся описывать виртуальную машину и ограничивать количество выполняемых инструкций).Rulexec
18.12.2016 12:51+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-комбинатором те же дела, это просто обобщённая функция, тип которой является запрещённым рекурсивным.
VoidEx
25.12.2016 20:31у меня есть правила, какие типы разрешены, а какие нет, но не буду их здесь описывать, если нужно — спрашивайте
А какие правила помимо того, что тип не должен стоять в отрицательной позиции?
leocat33
18.12.2016 09:22-1Это проблема цивилизации. И будет до тех пор, пока Я доминирует над МЫ.
user343
19.12.2016 00:30Пока у смертных разработчиков преобладают корыстные и личные мотивы, они будут «ваять» тлен и хлам на радость хакерам, дятлам и в топку энтропии.
Но в природе существуют программы биороботов, веками не устаревающих и без побочных эффектов.
«Верный мотив – работа на Общее Благо и Служение Жизни.
Неверный мотив – всё, что заставляет вас преследовать любые цели, принадлежащие физическому плану: слава, деньги, почёт, получение удовольствий, удовлетворение желаний.»
Hellsy22
19.12.2016 00:43+1За доминированием «мы» над «я» вам к муравьям и термитам. Они, кстати, освоили строительство, животноводство, сельское хозяйство, разделение на касты и т.д. Глядишь, через пару миллиардов лет и до программирования дорастут.
zzzcpan
18.12.2016 09:56+2Формальная верификация — это совсем не 100% гарантия, что программа работает корректно. Это способ перепроверить программу лишний раз, анализируя ее в другой плоскости другим методом, тем самым выявляя дефекты и уменьшая вероятность не раскрытых дефектов. Но не стоит забывать, что пока этим занимаются «земляне», они в доказательствах тоже могут допустить ошибки, некорректные допущения и т.д. История самой математики знает далеко не единицы таких ошибок. Поэтому верификация позволяет уменьшить частоту дефектов в коде на один-два порядка, но не избавиться от них полностью.
Важно понять, что смысл не в том, чтобы избавиться от всех дефектов, а в том, чтобы найти какой-то подход, который позволит избавиться от многих дефектов минимальными усилиями с учетом современных реалий. Формальная верификация тут не пройдет.worldmind
18.12.2016 09:59Формальная верификация это самый надёжный из доступных нам способов проверки.
А касательно минимизации влияния человека как раз свежий пост.zzzcpan
18.12.2016 19:19+2Нам не интересна проверка корректности ради проверки корректности. Нам интересно избавление от проблем, вызванных дефектами и формальная верификация в этом далеко не самый надежный способ, не стоит заблуждаться. А лишь один из инструментов повышения надежности, причем довольно узкоспециализированный.
worldmind
18.12.2016 19:22с вашими «аргументами» не поспоришь
funca
18.12.2016 20:26+1zzzcpan на самом деле говорит об базовых вещах. Таковы фундаментальные свойства всех формальных систем в отношении их интерпретаций. Если на пальцах, априорные тесты могут как угодно показывать, что программа их проходит в момент запуска тестов. Но они не могут гарантировать, что программа при эксплуатации делает именно то, что вам в данный момент времени хочется, чтобы она делала в текущем окружении.
Другими словами, наличие тестов не может поменять суть надежности, как вероятностной оценки, на что-то иное.worldmind
18.12.2016 20:29о какие тестах речь? я вроде ни о каких тестах не говорю
funca
18.12.2016 21:08+1Написал «тесты» на автомате. Как вы могли понять, формальной верификации все это относится в той же степени. Представьте программу для игры в шахматы, и как факт наличия формальной верификации кода будет влиять на исход конкретной партии.
qw1
19.12.2016 20:42+1Попробую объяснить другими словами.
Формальная верификация берёт два документа — текст программы и требования, записанные на некотором логическом языке, и доказывает их эквивалентность.
Проблема в том, что для сложных систем написание требований — то же программирование, где можно допустить тонны опечаток и ошибок.
По моему опыту, на Прологе можно сажать больше ошибок на строчку кода (концентрация нужна выше, и привычка). А спецификация, по сути, что-то типа Пролог-программы.
Казалось бы, двойная проверка. Но, чтобы программа «сошлась» с описанием, программист в случае проблем проконсультируется с составителем правил (если это не одно и то же лицо), и спросит, почему его программа не проходит проверку. Или тупо скопипастит логику из правил, подправит программу под спецификацию. А что если, он не так трактовал какое-то требование, как составитель спецификации (а на самом деле его трактовка была изначально правильной). В итоге, неверные допущения, когнитивные искажения, заблуждения проникнут и в требования, и в программу.
И, казалось бы, верифицированная программа, но глючить она тоже будет.
maniacscientist
18.12.2016 09:59Ну, с тем что нужно похудеть лишние слои я согласен.
А вот математически корректные программы — баба Яга против. Завтра мне может понадобиться взять в руки дебаггер чтобы остановить какое нибудь зарвавшееся сборище бизнесменов, программистов и инопланетян — а с такими программами это будет бесполезно.
EMS
18.12.2016 10:01+2— Кухонный нож! — объявил профессор и осекся. — Мнэ… Я планировал показать кухонный нож. Он куда более опасен, чем вилка. Но, видимо, слайды перепутаны, и здесь мы видим автомобиль. Внимание! Так называемый автомобиль! Это вид транспорта, управляемый вручную. В нем используется энергия взрыва, поэтому корпус начинен запасом жидкой взрывчатки. Движется автомобиль с огромной скоростью по специально выровненным лентам на поверхности планеты. При этом выделяет отравляющий газ. Надо ли продолжать? От хоминоида, управляющего автомобилем, требуется максимум внимания и сосредоточенности ежесекундно — каждый миг он рискует выехать за пределы ленты, столкнуться с другим транспортом или с хоминоидом, пересекающим ленту пешком. Это неминуемая гибель. Гибель несет и пребывание рядом с трубой автомобиля, выпускающей ядовитый газ. Да и сама конструкция транспорта так сложна и ненадежна, что немалое количество времени автомобиль проводит в ремонте. Простое перемножение вероятности поломки машины, секундной невнимательности (а хоминоиды очень невнимательны!) и непредвиденных дорожных ситуаций показывает, что вероятность гибели хоминоида в машине приближается к ста процентам в первый же час поездки! Кто не верит, может убедиться на любом компьютерном тренажере, имитирующем гонки, — аварии следуют одна за другой. Но! — Профессор торжествующе обвел взглядом притихшую равнину. — Хоминоиды годами, десятилетиями пользуются своей техникой! Аварии крайне редки и не обязательно ведут к смерти хоминоидов! Давайте следующий слайд!
За спиной раздался грохот, небо разом потухло, профессора швырнуло вперед на микрофонную стойку, и наступила темнота…
Итак, хоминоиды — Леонид Каганов
Areso
18.12.2016 12:02Как человек, часть работы которого заключается в той самой поддержки за деньги, могу сказать одну из причин, по которой моя работа почти наверняка будет с багами.
Её просто не проверяют. Ко мне приходит заявка (устно, письменно — не важно), я проверяю входные данные, у меня есть факт на выходе и то, что должно было получиться на выходе по идеи. Исправляю программу, отдаю. Далее автор заявки убеждается в том, что при тех данных, которые он подал на входе утром он получает правильный выход и закрывает заявку, но не проверяет ни предыдущие месяцы, ни другие комбинации различных настроек. В следующем месяце, с новыми данными и настройками, примерно 50-на-50, что результат будет некорректен и у меня появится очередная заявка от того же автора. И можно всю жизнь просидеть на такой техподдержке.
Примерно также то и дело прилетают заявки от людей, которые работают с передачей данных в смежные системы (или с получением данных от них), а общее количество систем, с которыми идет обмен данными, постоянно растет и уже превышает дюжину. Исправляем, проверяем этот месяц, ждем заявку в следующем месяце. Говнокод как он есть.funca
18.12.2016 20:38+1Для снижения вероятности регрессий, можете делать проверки системы по полной, согласно методикам приемо сдаточных испытаний (чек-листам, или как это у вас называют), после каждой модификации, а так же использовать автоматизацию тестирования для снижения стоимости этого процесса.
Vjatcheslav3345
18.12.2016 16:07+1Ирония судьбы заключается ещё и в том, что математика, ставшая формально строгой в недавнем историческом прошлом на глазах превращается в самую настоящую магию — старые кадры умирают или отходят от деятельности а молодёжь, сменяя их вынуждена браться за всё более и более сложные проблемы и, опять таки, чтобы хоть как то их решить использует, вынужденно, компьютеры — которые не идеальны ни с точки зрения софта, ни с точки зрения железа, ни с точки зрения формулировки проблемы. Думаю, без прорывов на данном фронте мы не сможем решать некоторые серьёзные проблемы.
В порядке шутки: новости дня «Сегодня [недалёкое светлое(?1) будущее], в 16-00 смыло деревню Гадюкино со всем населением. Наши информационные источники сообщают — причиной катастрофы была ошибка математической теоремы в программах местного Гидромета. Напомним, на прошлой неделе, из за аналогичных причин аппараты Breakthrough Starshot промазали мимо a-Центавра».
TimsTims
18.12.2016 16:41Люди говнокодят, но проблема не в людях, а в природе, которая тоже даёт баги. Вся мутация — это эксперименты между — прокатиться и выжил, или непрокатило — умер.
Ответ на все эти вопросы один, этот инструмент — математика
Которая тоже не совершенна на текущем уровне
gkvert
18.12.2016 19:24Есть такая картинка:
Так вот создать что-то быстро, дешево и качественно это утопия. Полное математическое покрытие тестами продукта? Чем больше в нём зависимостей, тем сильнее растет количество необходимых тестов. Так что людям приходится находить компромиссы.
DarkTiger
18.12.2016 20:25+1Ничто не ново под луной. Тема надежности ПО и аппаратуры, отдельно и в связке, обсуждается в инетах, и не только, регулярно. Вот, например, обзор на эту тему:
http://bodunov.org/images/stories/SC_Software.pdf
Да, есть стандарты на ПО в системах ответственного применения. Но сказать, что проблема состоит лишь в том, что плохие разработчики не желают следовать этим стандартам — это слишком смело. Потому что надо проверять сами стандарты, и самих проверятелей… и так до бесконечности. Еще римляне выразили всю сложность проблемы в фразе «Кто будет сторожить сторожей?»
Tazman
19.12.2016 00:09+1Покажите мне вакансию, связанную с формальной верификациейс, и я вам заплачу! Серьезно.
Формальная верификация — это очень круто и интересно. Мне бы очень хотелось работать в данной области. Но факт в том, что это никому не нужно. И вряд ли это станет мейнстримом в ближайшем будущем. Грусный смайлик.Rulexec
19.12.2016 00:23+2Пока в промышленности формальная верификация активно используется только в hardware, где цена ошибки крайне высока. И там это необходимо.
Apple, Intel (там ещё горстка других вакансий у них же), NXP, ARM.
И софтварные вакансии тоже иногда появляются, я уверен. И нужно быть готовым к такой, ибо ты не скажешь «ребята, у вас крутая вакансия, подождите, я тут три года попрактикуюсь и сразу к вам».Tazman
26.12.2016 18:30По-моему, верификация hardware — это вообще не про математику и не про доказательства.
Мне интересны именно «софтварные вакансии».
DarkTiger
19.12.2016 01:02+2Могу даже познакомить с живым представителем этого редкого вида :) Авионика, верификация VHDL кода MAC-ов всякоразных интерфейсов. Можете туда и устроиться :) Пишите в личку, если интересно.
Деньгами, что Вы мне обещали, пиво собеседнику оплатите, если есть желание пообщаться в Москве :)Tazman
26.12.2016 18:06Я смотрел в сторону VHDL, Verilog. Но у меня сложилось впечатление, что это к «формальной верификации» вообще не имеет никакого отношения. Это больше похоже на написание тестов для микросхем. А мне бы хотелось что-нибудь связанное именно с математическим доказательством корректности программ. Зависимые типы, все такое.
DarkTiger
26.12.2016 20:35А, вооот вам что надо :)
Это могу только посоветовать нагуглить на ВМК МГУ + Ваш запрос. Там этим занимаются, причем студенты — в обязательном порядке :)
Гуглите, списывайтесь с кафедрой системного программирования, а у них запросов на этот счет хватает, сведут Вас с интересными людьми. Там как раз стонут, что всем только базы данных нужны :)
stepik777
19.12.2016 00:13ставшее привычным, асимметричное шифрование выглядят как волшебство, хотя это лишь применение этого мощного инструмента.
Да, асимметричная криптография создана с применением математики, только ни у кого нет никакого доказательства, что современная асимметричная криптография надёжна, собственно как и доказательства того, что такую вообще можно создать (знаменитая проблема P ? NP).
Вообще, доказательство не панацея, оно лишь показывает, что программа соотвествует неким заданным критериям, но остаётся вопрос в том, являются ли эти критерии тем, что нужно. Есть популярная история о самолётах, летевших на высоте ниже уровня мирового океана, у которых из-за этого что-то заглючило. То есть программисты просто не подумали, что такое может быть. Если бы им нужно было доказать, что их софт работает нормально, то они точно также бы и доказали, что при высоте больше нуля всё работает отлично, но проблему бы это не решило.
Denkenmacht
19.12.2016 08:26Может кому интересно почитать будет, есть такая книжка — Стивен Спир "Догнать зайца". Там рассматривается в том числе практика устранения косяков в медучреждениях США и на флоте.
amarao
19.12.2016 11:44-1«Настоящие профессионалы» тоже делают ошибки. И учатся на них. /тред закрыт, дальше подвывания про «все не компетентные вот есть Настоящие Профессионалы, у которых нет так» — не актуальны.
PSIAlt
19.12.2016 16:21+1Статья никак не научная, однако с основными утверждениями согласен, для этого есть куча доказательств, которые и в 10 статей не влезут. Большинство софта из ряда вон кака, как и железо. Мне лично непонятно и удивительно как это все работает, хотя занимаюсь этим всем уже лет 15.
DarkTiger
20.12.2016 13:19В стандарте на автомобильные электронные системы ISO 26262 есть опция – Proven in use. Она позволяет избежать больших затрат на верификацию уже существующего ПО (и электроники). Эта опция применяется, когда известно о бессбойном функционировании ПО на автомобилях, находящихся в массовом производстве в течение предшествующего времени.
Вот, собственно, так все и работает :)
VoidEx
19.12.2016 22:53Так вроде математика — это тоже людское изобретение. Или в тех проектах, что вы описываете, её пока не применяют?
worldmind
22.12.2016 10:28Наверно не совсем про верификацию, но что-то близкое — Microsoft Terminator и вычислимость функций
stalinets
К сожалению, наводить порядок в говнокоде и тем более разрабатывать инструменты, исключающие появление говнокода — сейчас не в тренде и невыгодно. Всем надо подешевле, побыстрее, а ещё лучше — если код напишет кто-то другой (та же нейросеть). Ну так и получается, что иногда происходят катастрофы по вине плохого кода, плюс неэффективное расходование ресурсов.
Что должно случиться, чтобы приоритеты поменялись и математически доказанные программы вошли в моду?
worldmind
Думаю что тут необходимо влияние государства (групп государств) на бизнес, нужно выработать стандарты, которые не позволят в критических местах использовать плохокод.
Сегодня же есть какие-то процедуры сертификации, например, самолётов, нужно их сделать более строгими.
Lachezis
И в результате получить еще одну бюрократическую цепочку и сделать софт дороже.
worldmind
Да, но надо ли экономить на том что может стоить жизни или жизней?
Lachezis
Смотря с какой точки зрения смотреть, с экономической стоит, тут у нас чистая статистика.
worldmind
Кто это считал? Представим на минутку что из-за вируса весь цивилизованный мир оказался без электричества на неделю, какие будут убытки?
ankh1989
Теперь умножаем эти убытки на вероятность такого события, получаем изчезающе малую величину и спим спокойно. Вы ведь не ходите в каске от метеоритов?
worldmind
А как вы вычислили вероятность такого события?
Как та индейка у Талеба, которая думала что раз меня каждый день кормят, то так будет всегда, а вероятность казни топором исчезающе мала?
В каске не хожу, но считаю что противоастероидную систему для планеты разрабатывать нужно.
arheops
Тут не особо важна какая вероятность события, тут важнее, что не ее ПОЛНОЕ устранение у вас тупо не хватит ресурсов. Грубо говоря, вам тогда надо заняться защитой каждого индивидуума от метеоритов мегатонного класса. Справитесь?
worldmind
я не про индивидуальную защиту, я про защиту от катастроф, на голову может упасть и мелкий камень, от такого нам пока не по силам защититься, но не допустить падения таких, что могут вызвать ядерную зиму мы обязаны.
Tertium
пока по-крупному не долбанет, деньги не перенаправят. увы, пока экономически выгоднее делать код без гарантий (почитайте любое eula) и нет реальной ответственности, будет все как есть. как только станет невыгодно класть на критичный код, сразу найдут / придумают средства, даже если это на порядок замедлит работы. если непонятно, что и почему происходит, всегда дело в деньгах
Hellsy22
Причем, резко вырастет не только время разработки, но и стоимость единицы времени. Если разработчик будет нести личную ответственность, материальную или уголовную, то придется уравновешивать это чудовищными зарплатами. И то не факт, что на это согласятся хорошие специалисты, а не халявщики, которые будут надеяться на удачу.
bitlz
Стоимость не должна сильно изменится. Посмотрите на медицину. Многие медики несут личную, в том числе и уголовную ответственность. А зарплаты так себе.
Hellsy22
Только за совсем уж явные косяки. Многочисленные ошибки в диагнозе не считаются. В США от врачебных ошибок погибают более 200 тысяч человек ежегодно. И хочу отметить, что профессия врача в США оплачивается очень хорошо.
bitlz
Явные косяки? Возьмем к примеру анализы — ошибка в определении группы крови может привести к смерти пациента. Ошибочный анализ на генетическую совместимость пары может привести к рождению неполноценного ребенка.
И то и другое выполняется на потоке… То есть сидит человек и выдает по нескольку анализов в день. И за каждый подписывается.
В Челябинске, например, за такую работу платят от 15 (в гос лабораториях) до 30 (в частных) т.р.
qw1
Ни один человек не согласиться работать так, что совершая действия, в правильности которых он полностью уверен на момент их совершения, иметь возможность потом за это огрести.
Ответственность возможна только за отклонения от инструкций и норм. Там, где есть элемент творчества и работа интуиции (у тех же медиков — постановка диагнозов), ответственности нет.
bitlz
Ну вы хоть погуглите. Много случаев когда возбуждаются уголовные дела за неправильный диагноз повлекший за собой смерть пациента.
Hellsy22
А местный терапевт на любой кашель штампует «ОРЗ/ОРВИ».
Возьмем, к примеру, близкую для меня ситуацию — ГЭРБ, который проявлялся в постоянном кашле. Мне пришлось пройти около пяти обследований, дважды полежать в стационаре, прежде чем врачи поставили правильный диагноз. В перспективе ГЭРБ имеет высокие шансы привести к раку пищевода. И я уверен, что если бы дело дошло до рака, то никто из врачей, ставивших мне раз за разом неправильный диагноз, не понес бы ни уголовной, ни административной, ни даже финансовой ответственности.
Если же рассматривать не только смерть, но и инвалидность или получение перманентных последствий от неправильного лечения, то количество косяков вырастет на порядок.
Это я не к тому, что врачей нужно обязательно привлекать, а к тому, что в их работе косяки являются следствием характера и уровня организации самой работы. Иногда это приводит к смерти или инвалидности пациента. Но без врачей этих самых смертей и инвалидностей было бы на порядки больше.
msfs11
Вам не повезло с врачами, у меня же оба раза, когда я обращался к ЛОРу с больным горлом после непродолжительного лечения отправляли к гастроэнетрологу.
Tertium
ну, скажем так, ряды этот подход прорядит. соответственно вырастет цена работников. но тут еще скорее всего ужесточится отбор всякими сертификатами и т. д. ведь приятно, конечно, если человек несет ответственность, но даже если его расстрелять, миллиарды, вложенные в спутник не вернешь. скорее всего, есди сегмент «доказательного программирования» и появится, будет он ничтожной каплей в море.
касательно медиков — судя по договорам, какие я подписываю на всяких анализах и процедурах — это типа той же eula. чтобы медработник реально понес ответственность за что-то а) я должен быть депутатом или человеком с баблом, б) медработник должен сильно насолить коллегам, так, чтобы они захотели его слить.
ankh1989
Точно также как вы вычислили вероятность падения метеорита на голову и потому приняли решение не носить каску. Точно также как вы вычисляете вероятность серьёзных проблем от мороза -30 и принимаете решение одевать шапку, а не рассуждаете о планетарной системе защиты от морозов зимой.
worldmind
Вероятность падения метеорита на голову я рассчитать не могу, я просто ей пренебрегаю на свой страх и риск, этой мой выбор, от него не зависит судьба цивилизации.
А проблемы от мороза это не оценка неведомого, а вполне научные данные.
Priapus
https://en.wikipedia.org/wiki/Technology_readiness_level
Более строгими? У меня складывается впечатление, что вы не совсем понимаете, о чем пишите.
worldmind
т.е. у них всё настолько хорошо что аварий из-за багов в ПО не бывает?
Priapus
У кого у них? Вы сказали, что нужно выработать стандарты, я вам дал ссылку на стандарты. Потрудитесь объяснить, чем эти стандарты плохи, что в них вы хотите поменять и по какой причине.
worldmind
Ну например у NASA или ESA, плохи они тем, что не защищают от потери космический аппартов из-за программных ошибок.
Priapus
Дайте данные:
1. Что не защищают.
2. Какой процент потерь космических аппаратов происходит из-за программных ошибок и сколько это в денежном выражении (интересует именно процент потерь, обусловленный «программными ошибками», а не некорректными входными данными/данными с датчиков).
3. Сколько будет стоить защита по вашей методике и какой от этого будет профит.
Пока это балабольство какое-то. Все идиоты, один worldmind Д'Артаньян, который все лучше всех знает.
worldmind
Никого идиотами я не называл (и даже пояснил почему раньше этот путь не подходил) и честно сказал, что я не специалист, но из того, что я знаю и понимаю, логично вытекает описанное.
Исследований о проценте катастроф из-за багов в ПО не проводил, хотя думаю они есть (может lozga Zelenyikot Shubinpavel подскажут), вот несколько интересных случаев примеров.
Стоимость по тем же причинам точно оценить не могу, но тут приводил пример, вроде не такие уж астрономические затраты и вполне возможно что их ещё можно снизить повысив уровень автоматизации.
Shubinpavel
Собственно все ошибки из-за ПО что я вспомнил произошли из-за того, что просто не были в свое время учтены все обязательные правила при разработке систем. Просто не было сил, денег или времени чтобы прогнать все необходимые тесты на модели аппарата.
Исключения, только очень старые истории вроде компьютера Аполло которые не успевал обработать поступившие команды
При этом, си языки используются редко. Из тех, что я знаю, там больше наследников Паскаля. Например в США язык Ада, а у НПО Решетнева Модула-2.
worldmind
> Пока это балабольство какое-то. Все идиоты, один worldmind Д'Артаньян, который все лучше всех знает
напомнило
defaultvoice
Ой-вэй, ещё один этатист, считающий, что влиянием государств на бизнес можно решить все проблемы.
Давайте, я расскажу, что будет: самолеты продолжат падать, электричество отключаться, а метеориты падать на головы, но появится новая бюрократическая структура, которая съест часть налогов.
worldmind
С чего это новая? Хватит тех чьто есть сейчас, а может и меньше понадобится.
wOvAN
Более того, говно код прибыльней качественного кода, так как дешевле в написании, и можно бесконечно собирать деньги с пользователей за починку бесчисленных багов и продаже поддержки которая будет героически заставлять его работать.
Priapus
Есть завод, он производит, технически сложные штуки. Если он получит софт (пусть глючный и падучий), он сможет заптимизячить свои штуки (с геморроем, шутками и прибаутками, матами и т.д., но сможет) и на этом будет экономить олимпиард денег в год. Спросите у директора завода, хочет ли он получить такой софт сегодня, но с глюками или через год без глюков.
Я не сторонник говнокода, но реальность такова, что все хотят получить хоть как-то работающий софт сегодня и согласны им пользоваться пока вы его до завтра доработаете, а не сидеть и ждать до завтра, а то и до послезавтра, пока вы там все протестируете.
gkvert
Почему к сожалению? Говнокода ровно столько, сколько нужно экономике. Если вдруг окажется что говнокод уменьшает её эффективность, она начнёт больше инвестировать в нормальный код. Конечно всем бы нам хотелось получать максимально быстро новые качественные вещи за небольшие деньги, но это утопия.
Garbus
Ну тут получается маленькая проблема. Пока востребовано много говнокода, появляется много программистов соответствующего уровня. Будет как с микроскопом, превратить его в молоток на порядки проще, чем из молотка сделать оптический прибор. Все же переучивать человека выйдет скорее долго и дорого, а если еще и не у всех результат будет положительным…
P.S. Нынче зачастую купить качественную вещь непросто, даже имея приличные деньги. Просто потому, что их не деают массово, а единичные «ручные» стоят совсем уж неприлично.
Hellsy22
Кривая аналогия. Изначально у вас на руках не микроскоп и даже не молоток, а просто кусок камня — люди не рождаются профессиональными программистами.
Garbus
Вовсе нет. Камень получается уже огранен годами обучения и работы. Нет в некоторых пределах пластичность остается, но они не всегда достаточно большие.
Пожалуй приведу другой пример — столяр или плотник, вроде как оба работают с деревом. Но сможет ли тот, кто всю жизнь делал дома, вдруг сразу художественно вырезать орнамент на шкатулке? Или наоборот, всю жизнь делая художественные поделки, внезапно взять топор и так же быстро и качественно поставить баню?
Вот и выходит, даже если конкретный человек запросто переучится на «новые рельсы», это не обязательно случится быстро для всей отрасли. Отчего попытки изменить подход к делу выйдут просто чудовищными по затратам, если пытаться сделать это «мгновенно». А если добавить поговорку про «слабое звено» помноженную на текущий зоопарк решений, становится воистину печально.
VoidEx
Вы гистерезис не учли
potan
По моему, многим разработчикам просто не хватает образования, что бы понять такой подход (я как-то пробовал прочитать школьникам краткий курс Haskell и обнаружил что они не понимают что такое множество). Они свое непонимание передают менеджерам, и те не уделяют внимания качеству как чему-то недостижимому.
По этому я считаю, что надо всем, особенно программистам, учить математику (матлогику, алгебру, теорию категорий) — тогда внедрение верификации пойдет легче.
5oclock
Если учить математику, то когда разбираться с собственно программированием? :)
Современному программисту и так постоянно приходится разбираться с чем-то новым в программировании плюс — погружаться в новые предметные области: собственно что он программирует.
Тут уж скорее нужно математикам не абстракциями рассказывать, которыми они в своей среде оперируют, а «опускаться» на уровень программистов и, грубо говоря, делать методички для не математиков. Пусть и с определённой подготовкой в виде курса математики в ВУЗе. Который они уже основательно подзабыли.
А если спускать инженерам (в любой, кстати области) какую-то абстрактную математику, то и не будут они её использовать. Просто даже не поймут — как?
И будут дальше делать: по наитию, как привыкли, как переняли у коллег…
potan
Пора уже перестать спешить. Все равно в ближайшее время простой программист не сможет конкурировать с ИИ и/или дешевыми программистами из стран третьего мира.
Правильно, если надо учиться на программиста не пять, а все десять лет, с глубоким изучением сложных абстрактных дисциплин. Искусственные нейронные сети с этим еще не скоро справятся, а компановать из готовых модулей скоро научатся.
worldmind
Кодерам оставить просто программирование, а специалисты с высшим образованием должны думать о более сложных задачах.
5oclock
А что значит «просто программирование»?
worldmind
То программирование, которое не требует знаний математики
5oclock
Откройте любую книгу по программированию — там какая-то специальная математика не особо-то нужна.
Снизу доверху: от кодера до руководителя проекта.
Теоретизирования из области информатики или математики к прикладному программированию отношения имеют лишь постольку поскольку из них, в итоге, формулируются конкретные алгоритмы или рекомендации для ежедневной работы программистов.
Вы каждый день интегралы по поверхности не берёте, а пользуетесь готовыми формулами, которые вам вывели математики.
worldmind
Я как-то думал над тем, что должен знать программист с высшим образованием и надумал такой список, буду рад замечаниям и merge request'ам.
potan
На мой взгляд просто обобщенный хороший программист (не только ученый) все-таки должен знать лямбда-исчисление и теорию категорий, основы криптографмм и блокчейна, и понимать что из себя представляет доказательство правильности.
А вот последние 4 пункта из общиепрограммстких, и биоинформатика из «для ученых», на мой взгляд, слишком специфичны и не всем обязательны.
Да, машинное обучение для ученых надо знать, но простые программисты могут его обойти стороной.
worldmind
Да, биоинформатику только в трендах нужно оставить, представлению нужно иметь. А машинное обучение набирает обороты, надо заранее начать учить.
potan
Я думаю, что в ML все еще много раз поменяется. Сейчас там практически одни нейронные сети. Вы правильно отметили, что они трудно верифицируются. По этому я жду появления/возраждения чего-то типа Индуктивного логического программирования. А может оно пойдет в сторону скрытых марковских моделей, или еще куда.
worldmind
Да вот есть риск, что определённый класс задач решается только структурами а-ля мозг с присущими ему недостатками. Хотя я был бы рад если бы для них нашлись строгие решения.
5oclock
А где в своей работе ему всё это применять?
potan
Например, выучить язык, для понимания которого эта математика полезна, и писать на нем код.
5oclock
А он сейчас пишет код и проектирует системы.
На других языках.
Зачем ему изучать некую специфическую математику с перспективой, что пригодится она только для того, чтобы изучить такой же специфический язык программирования?
И много программистов, для которых программирование — профессия (деньги они этим зарабатывают) — много их станет изучать эту специальную математику, чтобы впоследствии въехать в такой же «математизированный» язык?
potan
Что бы софт становился более надежным.
Языки, не основанные явно на математике, не способствуют написанию надежного софта.
Да и в C++ то же виртуальное наследование хорошо описывается теорией категорий, и знающие ее сможет применять его более осмыслено.
5oclock
А в «языке основанном на математике» нельзя ошибку сделать?
Сотни тысяч программистов с++ и сейчас применяют виртуальное наследование вполне осмысленно. Может даже ближе к его реализации, чем если бы они думали об этом как-то математизированно, с применением абстрактных теорий.
potan
Мой опфт говорит, что на Haskell подавляющее большинство ошибок ловится во время компиляции. Вероятно, Rust ведет себя похоже.
На счет сотен тысяч программистов я сильно сомневаюсь.
5oclock
Ну так в любом компилируемом языке программирования подавляющая часть ошибок ловится на этапе компиляции :)
potan
Вы пробовали сравнивать?
5oclock
Что с чем сравнивать? :)
potan
Разные компилируемые языки на предмет доли нахйденых ошибок при компиляции.
5oclock
Так тут и сравнивать нечего.
Ошибки, вылавливаемые компиляторами, это опечатки и нарушения синтаксиса. Это же очевидно :)
Логические и алгоритмические ошибки они не могут обнаружить: компилятор же не знает что именно имеет ввиду программист.
Хотя в С/С++ полезно читать предупреждения. Бывает за ними скрывается часть этих ошибок.
Может в «математических» языках более чётко поставлена работа с ресурсами и уменьшены другие возможности «выстрелить себе в ногу», но это же как я понимаю не благодаря их «математичности».
И в «вольных» языках если придерживаться известных техник программирования — можно уменьшить количество таких ошибок во много раз, если не извести совсем.
qw1
На ассемблере никогда не писали? Там тоже можно придерживаться известных техник, чтобы совершать меньше ошибок.
5oclock
На заре своего програмёрства было дело.
Но техник особых не знал.
qw1
Сравнивая ассемблер и С++, язык влияет на количество ошибок в программе?
5oclock
Программы очень разные.
На ассемблере такие программы, как на C++ — замучаешься писать.
На нём я не писал какую-то сложную обработку данных, пользовательский интерфейс.
Они более… прямолинейные что-ли. Не очень много ветвлений, условий всяких. И более выверенные были.
В общем, сложно сравнить.
Alexeyslav
Опечатки и синтаксис это такая мелочь что и за ошибки считать не стоит. А вот перепутать переменные местами, или нечаянно в цикле изменить переменную-счётчик этого же цикла, или нечаянно изменить константу — такие ошибки вам ни один из обычных компиляторов не словит, разве что какой-то глубокий анализ нейронной сетью… а вот такие языки как Haskel, Rust и тому подобные не позволят сделать таких глупых ошибок не позволив даже скомпилировать программу.
5oclock
Серьёзно?
Это — да, хороший контроль.
А как это в haskell'е сделано?
А насчёт в цикле не изменить переменную-счётчик…
Это будет покруче запрета goto :)
qw1
5oclock
Не-не. Погодите.
Функцию можно в хаскеле объявить? С 2-3 переменными одинакового типа? (типы же там есть? Он же жёстко типизированный язык?)
И вот при вызове функции — можно вместо, грубо говоря, (x, y, z) передать (x, x, z) или (x, z, y)?
qw1
Эти ошибки компилятор не ловит.
5oclock
Остаётся дождаться комментария от Alexeyslav — какое перепутывание переменных он имел ввиду.
potan
Кстати, Rust в некоторых случаях передачу (x,x,z) вместо (x,y,z) отловит :-).
Но в том то и дело, что такие функции прихолится объявлять не часто.
У меня в Haskell несколько раз допускалась ошибка, которую пришлось дебажить, типа let n1 = n+1 in ..., где в… скописченый код, в котором я не все n заменил на n1. Ради таких случаев я даже выраьотал технику писать вместо let такую конструкцию case n+1 of n ->…
5oclock
А n у Вас при этом тоже использовалось и оказалось того же типа, что и n1?
potan
Использовалось, но не должно было. Несколько раз требовалось выполнить похожий код и для целого числа n, и для n+1, а выделять его в отдельную функцию было лень или не очень удобно. Пришлось изобретать способы маскировать старую версию переменной.
Alexeyslav
Именно. Потому что многие компиляторы идут на хитрость и константы на самом деле переменные, к которым запрещено напрямую обращаться. Или константы-объекты которые передаются в функцию по ссылке… и ничто не мешает коду внутри изменить этот объект при помощи манипуляций с указателями(напрямую-то компилятор ругнётся).
Изменять счётчик цикла — это великое зло чреватое граблями, и да оно похуже использования goto… поэтому придумали такие штуки как итераторы, в которых нет доступа к этому счётчику и накосячить нереально. Но итераторы начинают проникать и в классические языки, но опять же как-то местами очень костыльно.
5oclock
Речь была про:
Так вот нечаяно — тебе ни один компилятор не даст изменить. И — да, именно на этапе компиляции.
А если ты const_cast'ами направо и налево размахиваешь — ну так это ты сам себе злобный буратин.
И какая программисту разница как именно внутри runtime реализована константа? Для тебя она — константа.
Если конечно ты всё-таки не захочешь странного.
А в хаскеле наверное указателей и X-cast'ов нет?
Ну а про счётчик цикла — это просто какая-то более сильная религия чем даже запрет goto :)
Alexeyslav
Разницы-то оно конечно нет, но почему-то проблема которое десятилетие очень остро стоит. Разница наверно в том что в одном языке приходится постоянно костылями пользоваться а в другом нет.
Конечно, лучше ошибок не делать быть здоровым и богатым. Но статистика вещь упрямая, почему-то люди упорно не хотят сочетать все эти факторы и регулярно гуляют по полям из грабель.
5oclock
Проблема модификации констант?
Мне кажется Вы надумываете лишнего.
Я за 20 лет программирования ни разу с такой проблемой не сталкивался.
Да и в коде эти места будут шиты белыми нитками: не зря же const_cast придуман.
potan
Все преобразования типов в Haskell явные. И не константных величин нет.
5oclock
А вот там выше приводили пример с n1 и n.
Это что?
potan
Формально говоря, именованные величины некоторого типа, относящего к классу типов Num (раз для них определен (+)). Но в речи все их называют переменными, хотя изменяться они не могут.
5oclock
А что значит?
potan
Попытаться определить величину n, которая равна себе плюс один. Скорее всего окончится ошибкой runtime при попытке его использовать (если не определить хитрый тип, для которго это уравнение имеет решение и компилятор сможет его вывести). Но написать такое случайно маловероятно и эта ошибка легко найдется.
В других языках, таких как SML, OCaml, F# (а так же Racket, хоть он не из этой серии) различают конструкции let и let rec — первая создаст новую величину n, равную старой величине n+1, и с новой областью видимости. Вторая выдаст ошибку компиляции, поскольку не умеет решать такие уравнения.
5oclock
Да-а… brainfuck прям какой-то…
potan
Наоборот, все выглядит как на бумаге математически задачу описываешь.
VoidEx
Так математика ж brainfuck и есть :) Но в хорошем смысле этого слова
zzzcpan
Берите любой большой проект на Haskell или Rust и смотрите, дефектов там не меньше, чем у других. Формальная верификация такого кода тоже может заметно уменьшить их количество.
Просто причина совсем не в математике, причина в сложности, которой «земляне» могут оперировать. И если атаковать одну и ту же проблему двумя принципиально разными методами или на двух совершенно разных уровнях для подстраховки, то при вероятности ошибки 0,01 в каждой строчке обоих методов мы все равно снижаем вероятность одновременного присутствия ошибок в обоих до 0.01*0,01, т.е. до 0.0001. В этом вся суть.
potan
Интерсно сравнить.
На моем опыте в двух сравнимых проектах — модель суперскалярного процессора MIPS на Haskell и прочессора с архитектурой потока данных на C++ — дефектов в первом было меньше. Правда, мнение субективное, я в обоих проектах участвовал.
Hellsy22
Давайте по пунктам.
1. Способность логично и алгоритмически мыслить — не формализуется и не измеряется.
2. Код хорошо читаемый кем конкретно? Если специалистом в той же области и того же уровня, то это одно, а если даже новичками или волонтерами — совсем другое. Слишком размыто.
3. Неконкретно.
4. А всезнанием и просветлением он обладать не должен? Хорошо, когда специалист хорошо знает хотя бы несколько популярных технологий и инструментов и имеет представление о еще полудесятке.
5. Да что уж, пусть сразу знает топологию всех используемых чипов и детали процесса производства.
6. Все программисты способны разрабатывать все. Вопрос во времени и эффективности.
7. С базовыми принципами работы баз данных можно ознакомиться за три минуты в вики. Получить реальный опыт работы с БД в проектах с высокой нагрузкой или высокой сложностью — совсем другое дело.
И дальше все примерно так же. Все это совершенно не важно, поскольку отражает лишь субъективное восприятие собственного опыта. А раз так, то зачем изобретать очередной велосипед на костылях — возьмите какой-нибудь типичный опросник для программистов типа Programmer skill matrix (их много разных уже придумали).
Что особенно забавно, так это то, что в вашем видении «специалист высокого класса» не должен иметь представления о командной работе и документировании кода. Этим, дескать, должен заниматься лишь руководитель.
worldmind
1. Тесты на логику и задачи на программирование
2. Читаемый всеми, средним специалистом
> «специалист высокого класса» не должен иметь представления о командной работе и документировании кода
это всего-лишь группировка скилов по типам, это не значит что кто-то не должен знать
Hellsy22
1. «Задача на программирование» звучит примерно так же странно как «задача на науку». Программирование охватывает огромное количество областей.
2. «Средний специалист» — это тоже абстракция. В разных компаниях разное понятие «среднего». Вполне возможно, что того, кого вы считаете средним специалистом, кто-то будет считать высококлассным, а кто-то такого даже стажером не возьмет.
msfs11
Пример из жизни: по тестам человек отлично все знает, но отсутствие реального опыта просто не дает ему решать целый класс задач.