Comments 306
Что должно случиться, чтобы приоритеты поменялись и математически доказанные программы вошли в моду?
Сегодня же есть какие-то процедуры сертификации, например, самолётов, нужно их сделать более строгими.
Как та индейка у Талеба, которая думала что раз меня каждый день кормят, то так будет всегда, а вероятность казни топором исчезающе мала?
В каске не хожу, но считаю что противоастероидную систему для планеты разрабатывать нужно.
И то и другое выполняется на потоке… То есть сидит человек и выдает по нескольку анализов в день. И за каждый подписывается.
В Челябинске, например, за такую работу платят от 15 (в гос лабораториях) до 30 (в частных) т.р.
Ответственность возможна только за отклонения от инструкций и норм. Там, где есть элемент творчества и работа интуиции (у тех же медиков — постановка диагнозов), ответственности нет.
Возьмем, к примеру, близкую для меня ситуацию — ГЭРБ, который проявлялся в постоянном кашле. Мне пришлось пройти около пяти обследований, дважды полежать в стационаре, прежде чем врачи поставили правильный диагноз. В перспективе ГЭРБ имеет высокие шансы привести к раку пищевода. И я уверен, что если бы дело дошло до рака, то никто из врачей, ставивших мне раз за разом неправильный диагноз, не понес бы ни уголовной, ни административной, ни даже финансовой ответственности.
Если же рассматривать не только смерть, но и инвалидность или получение перманентных последствий от неправильного лечения, то количество косяков вырастет на порядок.
Это я не к тому, что врачей нужно обязательно привлекать, а к тому, что в их работе косяки являются следствием характера и уровня организации самой работы. Иногда это приводит к смерти или инвалидности пациента. Но без врачей этих самых смертей и инвалидностей было бы на порядки больше.
касательно медиков — судя по договорам, какие я подписываю на всяких анализах и процедурах — это типа той же eula. чтобы медработник реально понес ответственность за что-то а) я должен быть депутатом или человеком с баблом, б) медработник должен сильно насолить коллегам, так, чтобы они захотели его слить.
Более строгими? У меня складывается впечатление, что вы не совсем понимаете, о чем пишите.
1. Что не защищают.
2. Какой процент потерь космических аппаратов происходит из-за программных ошибок и сколько это в денежном выражении (интересует именно процент потерь, обусловленный «программными ошибками», а не некорректными входными данными/данными с датчиков).
3. Сколько будет стоить защита по вашей методике и какой от этого будет профит.
Пока это балабольство какое-то. Все идиоты, один worldmind Д'Артаньян, который все лучше всех знает.
Исследований о проценте катастроф из-за багов в ПО не проводил, хотя думаю они есть (может lozga Zelenyikot Shubinpavel подскажут), вот несколько интересных случаев примеров.
Стоимость по тем же причинам точно оценить не могу, но тут приводил пример, вроде не такие уж астрономические затраты и вполне возможно что их ещё можно снизить повысив уровень автоматизации.
Исключения, только очень старые истории вроде компьютера Аполло которые не успевал обработать поступившие команды
При этом, си языки используются редко. Из тех, что я знаю, там больше наследников Паскаля. Например в США язык Ада, а у НПО Решетнева Модула-2.
Я не сторонник говнокода, но реальность такова, что все хотят получить хоть как-то работающий софт сегодня и согласны им пользоваться пока вы его до завтра доработаете, а не сидеть и ждать до завтра, а то и до послезавтра, пока вы там все протестируете.
P.S. Нынче зачастую купить качественную вещь непросто, даже имея приличные деньги. Просто потому, что их не деают массово, а единичные «ручные» стоят совсем уж неприлично.
Будет как с микроскопом, превратить его в молоток на порядки проще, чем из молотка сделать оптический прибор
Кривая аналогия. Изначально у вас на руках не микроскоп и даже не молоток, а просто кусок камня — люди не рождаются профессиональными программистами.
Пожалуй приведу другой пример — столяр или плотник, вроде как оба работают с деревом. Но сможет ли тот, кто всю жизнь делал дома, вдруг сразу художественно вырезать орнамент на шкатулке? Или наоборот, всю жизнь делая художественные поделки, внезапно взять топор и так же быстро и качественно поставить баню?
Вот и выходит, даже если конкретный человек запросто переучится на «новые рельсы», это не обязательно случится быстро для всей отрасли. Отчего попытки изменить подход к делу выйдут просто чудовищными по затратам, если пытаться сделать это «мгновенно». А если добавить поговорку про «слабое звено» помноженную на текущий зоопарк решений, становится воистину печально.
По этому я считаю, что надо всем, особенно программистам, учить математику (матлогику, алгебру, теорию категорий) — тогда внедрение верификации пойдет легче.
Современному программисту и так постоянно приходится разбираться с чем-то новым в программировании плюс — погружаться в новые предметные области: собственно что он программирует.
Тут уж скорее нужно математикам не абстракциями рассказывать, которыми они в своей среде оперируют, а «опускаться» на уровень программистов и, грубо говоря, делать методички для не математиков. Пусть и с определённой подготовкой в виде курса математики в ВУЗе. Который они уже основательно подзабыли.
А если спускать инженерам (в любой, кстати области) какую-то абстрактную математику, то и не будут они её использовать. Просто даже не поймут — как?
И будут дальше делать: по наитию, как привыкли, как переняли у коллег…
Правильно, если надо учиться на программиста не пять, а все десять лет, с глубоким изучением сложных абстрактных дисциплин. Искусственные нейронные сети с этим еще не скоро справятся, а компановать из готовых модулей скоро научатся.
Снизу доверху: от кодера до руководителя проекта.
Теоретизирования из области информатики или математики к прикладному программированию отношения имеют лишь постольку поскольку из них, в итоге, формулируются конкретные алгоритмы или рекомендации для ежедневной работы программистов.
Вы каждый день интегралы по поверхности не берёте, а пользуетесь готовыми формулами, которые вам вывели математики.
А вот последние 4 пункта из общиепрограммстких, и биоинформатика из «для ученых», на мой взгляд, слишком специфичны и не всем обязательны.
Да, машинное обучение для ученых надо знать, но простые программисты могут его обойти стороной.
На мой взгляд просто обобщенный хороший программист (не только ученый) все-таки должен знать лямбда-исчисление и теорию категорий
А где в своей работе ему всё это применять?
На других языках.
Зачем ему изучать некую специфическую математику с перспективой, что пригодится она только для того, чтобы изучить такой же специфический язык программирования?
И много программистов, для которых программирование — профессия (деньги они этим зарабатывают) — много их станет изучать эту специальную математику, чтобы впоследствии въехать в такой же «математизированный» язык?
Языки, не основанные явно на математике, не способствуют написанию надежного софта.
Да и в C++ то же виртуальное наследование хорошо описывается теорией категорий, и знающие ее сможет применять его более осмыслено.
Что бы софт становился более надежным.
Языки, не основанные явно на математике, не способствуют написанию надежного софта.
А в «языке основанном на математике» нельзя ошибку сделать?
Да и в C++ то же виртуальное наследование хорошо описывается теорией категорий, и знающие ее сможет применять его более осмыслено.
Сотни тысяч программистов с++ и сейчас применяют виртуальное наследование вполне осмысленно. Может даже ближе к его реализации, чем если бы они думали об этом как-то математизированно, с применением абстрактных теорий.
На счет сотен тысяч программистов я сильно сомневаюсь.
Ошибки, вылавливаемые компиляторами, это опечатки и нарушения синтаксиса. Это же очевидно :)
Логические и алгоритмические ошибки они не могут обнаружить: компилятор же не знает что именно имеет ввиду программист.
Хотя в С/С++ полезно читать предупреждения. Бывает за ними скрывается часть этих ошибок.
Может в «математических» языках более чётко поставлена работа с ресурсами и уменьшены другие возможности «выстрелить себе в ногу», но это же как я понимаю не благодаря их «математичности».
И в «вольных» языках если придерживаться известных техник программирования — можно уменьшить количество таких ошибок во много раз, если не извести совсем.
Но техник особых не знал.
… нечаянно изменить константу
… такие ошибки вам ни один из обычных компиляторов не словит
Серьёзно?
перепутать переменные местами
Это — да, хороший контроль.
А как это в haskell'е сделано?
А насчёт в цикле не изменить переменную-счётчик…
Это будет покруче запрета goto :)
А как это в haskell'е сделано?Большим уровнем абстракции. Выбрать из коллекции элементы по фильтру, отсортировать, провести какие-то изменения в каждом отобранном элементе — и всё в одну строчку, где ошибиться сложнее, чем расписывая циклы через итераторы над коллекциями.
Функцию можно в хаскеле объявить? С 2-3 переменными одинакового типа? (типы же там есть? Он же жёстко типизированный язык?)
И вот при вызове функции — можно вместо, грубо говоря, (x, y, z) передать (x, x, z) или (x, z, y)?
Но в том то и дело, что такие функции прихолится объявлять не часто.
У меня в Haskell несколько раз допускалась ошибка, которую пришлось дебажить, типа let n1 = n+1 in ..., где в… скописченый код, в котором я не все n заменил на n1. Ради таких случаев я даже выраьотал технику писать вместо let такую конструкцию case n+1 of n ->…
У меня в Haskell несколько раз допускалась ошибка, которую пришлось дебажить, типа let n1 = n+1 in ..., где в… скописченый код, в котором я не все n заменил на n1
А n у Вас при этом тоже использовалось и оказалось того же типа, что и n1?
Изменять счётчик цикла — это великое зло чреватое граблями, и да оно похуже использования goto… поэтому придумали такие штуки как итераторы, в которых нет доступа к этому счётчику и накосячить нереально. Но итераторы начинают проникать и в классические языки, но опять же как-то местами очень костыльно.
нечаянно изменить константу
Так вот нечаяно — тебе ни один компилятор не даст изменить. И — да, именно на этапе компиляции.
А если ты const_cast'ами направо и налево размахиваешь — ну так это ты сам себе злобный буратин.
И какая программисту разница как именно внутри runtime реализована константа? Для тебя она — константа.
Если конечно ты всё-таки не захочешь странного.
А в хаскеле наверное указателей и X-cast'ов нет?
Ну а про счётчик цикла — это просто какая-то более сильная религия чем даже запрет goto :)
Конечно, лучше ошибок не делать быть здоровым и богатым. Но статистика вещь упрямая, почему-то люди упорно не хотят сочетать все эти факторы и регулярно гуляют по полям из грабель.
Это что?
let n=n+1
В других языках, таких как SML, OCaml, F# (а так же Racket, хоть он не из этой серии) различают конструкции let и let rec — первая создаст новую величину n, равную старой величине n+1, и с новой областью видимости. Вторая выдаст ошибку компиляции, поскольку не умеет решать такие уравнения.
Просто причина совсем не в математике, причина в сложности, которой «земляне» могут оперировать. И если атаковать одну и ту же проблему двумя принципиально разными методами или на двух совершенно разных уровнях для подстраховки, то при вероятности ошибки 0,01 в каждой строчке обоих методов мы все равно снижаем вероятность одновременного присутствия ошибок в обоих до 0.01*0,01, т.е. до 0.0001. В этом вся суть.
1. Способность логично и алгоритмически мыслить — не формализуется и не измеряется.
2. Код хорошо читаемый кем конкретно? Если специалистом в той же области и того же уровня, то это одно, а если даже новичками или волонтерами — совсем другое. Слишком размыто.
3. Неконкретно.
4. А всезнанием и просветлением он обладать не должен? Хорошо, когда специалист хорошо знает хотя бы несколько популярных технологий и инструментов и имеет представление о еще полудесятке.
5. Да что уж, пусть сразу знает топологию всех используемых чипов и детали процесса производства.
6. Все программисты способны разрабатывать все. Вопрос во времени и эффективности.
7. С базовыми принципами работы баз данных можно ознакомиться за три минуты в вики. Получить реальный опыт работы с БД в проектах с высокой нагрузкой или высокой сложностью — совсем другое дело.
И дальше все примерно так же. Все это совершенно не важно, поскольку отражает лишь субъективное восприятие собственного опыта. А раз так, то зачем изобретать очередной велосипед на костылях — возьмите какой-нибудь типичный опросник для программистов типа Programmer skill matrix (их много разных уже придумали).
Что особенно забавно, так это то, что в вашем видении «специалист высокого класса» не должен иметь представления о командной работе и документировании кода. Этим, дескать, должен заниматься лишь руководитель.
2. Читаемый всеми, средним специалистом
> «специалист высокого класса» не должен иметь представления о командной работе и документировании кода
это всего-лишь группировка скилов по типам, это не значит что кто-то не должен знать
2. «Средний специалист» — это тоже абстракция. В разных компаниях разное понятие «среднего». Вполне возможно, что того, кого вы считаете средним специалистом, кто-то будет считать высококлассным, а кто-то такого даже стажером не возьмет.
Например, я столкнулся с проблемой — нужен был счетчик импульсов на 12 разрядов. Большая часть микросхем мелкой логики, на которой его можно построить, уже снята с производства. И на меня смотрели как на идиота — мол, делай на МК и все. Один корпус вместо двух десятков и прочее. Но мне нужна была абсолютная устойчивость (помехи, МК может виснуть, железное решение, стоявшее там до этого не висло при грамотной экранировке совсем и никогда), плюс еще некоторые хитрые параметры. Почему «железячные» решения исчезают в угоду софту — мне непонятно. Но это меня не радует.
При этом МК может творить всякие чудеса от перескока на совершенно неожиданную ветку программы вплоть до полного зависания, выдернуть из которого его может только отключение питания.
К сожалению, в реальности и с включенным watchdog таймером МК порой намертво зависает. Реже, чем без него, но всё-таки зависает.
Возьмём к примеру классический счётчик джонсона(561ИЕ8), который может иметь запрещённые(невалидные) состояния, наведённые помехами и только специально спроектированная схема позволяет счётчику выйти в одно из рабочих состояний за конечное количество тактов.
Если взять более сложные схемы на логике(Привет ПЛИС) то там так же достаточно много «программных заморочек» где что-то может пойти не так. Даже обычный триггер можно манипуляциями входных сигналов ввести в невалидное состояние. Попробуйте узнать для чего вообще придумали двойные(с двойной защелкой) D-триггеры. И всё это является примером того как в программах преодолевают сбои, только на аппаратном уровне. И даже двойная защёлка не убирает аппаратную проблему простого триггера а только лишь уменьшает вероятность её возникновения.
А ещё есть race condition…
Это известная литературная мистификация.
В прикладных программах всегда были баги. В картриджах для игровых приставок (ПЗУ, новую версию не накатишь) были баги, в операционных системах со времён их появления были баги, в микрокодах процессоров были, да даже в топологии процессоров были баги.
На военных спутниках и самолётах были баги, и это несмотря на смехотворный по нынешним меркам объём кода, простой как топор процессор и 10 колец оцепления со всеми существующими способами их устранения.
Не было никогда безглючного софта и не будет никогда. Это фундаментально невозможно.
А тем, кому не нравится «коммерциализация», можно предложить альтернативу — вы будете покупать железо, которое стоит как ваша квартира? Игры не за 4 тысячи, а за 40? Пустой интернет, потому что все профессора информационных технологий в стране завалены заказами на год вперёд. Всеми 10-ю заказами? Прикладной софт, не обновляющийся десятилетиями по этой-же причине? А то, что его ещё и меньше будет на пару порядков?
И всё это ради того, чтобы частота возникновения ошибок сократилась с «1 раз в неделю» до «1 раз в год».
На сам-то деле всё проще. Программа (и железо) нужна чтобы решать какую-то задачу, у неё нет самоцели быть правильной. Глюков, багов и недоработок в ней будет ровно столько, сколько экономически обоснованно. Всегда есть предел, после которого затраты на дальнейшее улучшение начинают превосходить полезный эффект от этих изменений.
Для написания более сложного безглючного софта существуют специальные методики(см. formal verification).
Другое дело, что методики не защищают от архитектурных или логических ошибок.
С чем я могу полностью согласиться, так это с тем, что безглючный софт комерчески совершенно не целесообразен.
Что убирает сразу много классов задач(те же игры становятся очень дорогими) и как результат полностью убирает экономический смысл улучшения архитектуры(и фраза деректора IBM про рынок компьютеров в размере 5 штук на планету становится правдой).
Кому нужен микроконтроллер с лампочками, если верификация его ПО потребует суперкомпьютера(ВЕРИФИЦИРОВАННОГО с верифицированным ПО), которого ни у кого нет.
Возмите микроконтроллер который вам будет азбукой морзе лампочкой мигать.
… который глюканёт при сбое питания. Попытаетесь предотвратить это событие — наткнётесь на баг аппаратной части этого контроллера (которых немеряно, почитайте даташиты в конце). Закажете партию МК без этих багов — получите мигалку космической приёмки по цене топового смартфона.
Кроме того, то что я не просто так написал «программа и есть наиболее полное формальное описание, как должно быть правильно». Если у вас верификация более проработана, чем программный код, то она фактически становится первичным исходником программы, по которому строится всё остальное. И мы снова упираемся в то, с чего начали, как проверить, что мы при верификации учли все возможные ошибки, если её результат — это самое исчерпывающее описание программы?
Просто вы написали «есть такая метода чтобы свести ошибки почти к нулю» и началось: «а вот как хорошо раньше было», «а ведь можно же всё делать хорошо», «какую
А то, что эта метода имеет имеет астрономическую стоимость, да к тому же тоже не без изъяна, и поэтому в «повседневной работе» не особо применима, все как-то из виду упускают.
«стиль программирования под названием формальное подтверждение. В отличие от обычного кода, написанного неформально и оцениваемого обычно только по его работоспособности, формально подтверждённое ПО выглядит, как математическое доказательство: каждое утверждение логически вытекает из предыдущего. Всю программу можно проверить с той же уверенностью, что и математическую теорему.»
https://geektimes.ru/post/282234/
У вас сейчас статически типизированные программы типизированы не полностью. Т.е. у вас в наличии функции типа
«принимает массив с элементами типа T и число, возвращает элемент типа T или создаёт исключение»
.А в более мощных системах типизации (где есть зависимые типы) можно иметь функции типа
«принимает массив длины n с элементами типа T, число m, которое больше либо равно нуля, строго меньше n, возвращает элемент типа T»
.И тогда вам нужно будет передавать в эту функцию значения типа
«m меньше n»
, чтобы ваша программа вообще смогла скомпилироваться.И так можно описывать абсолютно что угодно, включая то, как должны обрабатываться внешние события, хотя никто не верит.
По личному опыту самое простое это использование prerequest в начале метода (к примеру из guava). Но в любом случае это не compile-time validation.
Массив n элементов типа T
.И никто не мешает использовать эту n в рантайме.
Просто чтобы обращаться потом к произвольным элементам массива действительно нужно будет делать явные проверки времени исполнения, чтобы получить доказательство того, что индекс действительно меньше (но если потом, к примеру, использовать числа, которые меньше проверенного, то больше проверок делать не нужно будет, ибо можно будет доказать этот факт и проверка в итоге будет только первая).
Но, например, если мы просто хотим обойти весь массив, то если мы устроим цикл от 0 до n — нам не потребуется ничего проверять, т.к. будет тривиально получить пруф того, что индекс будет меньше n, ибо нам его генерит цикл и никуда не меняет больше.
Буду дома, может накидаю какой пример кода, как именно оно будет проверяться.
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 тут, кстати, не уникальна.
К счастью, это не на столько частая ошибка, если с массивами в основном работать с помощью инетретором и отлаженных функций высжего порядка (map, fold и тп).
В любом случае, математика не идеальна. Это ещё тов. Гёдель показал, а вот что с этим делать другой вопрос. И да, она может ошибаться, теоремы могут быть ошибочны, а их предпосылки логически неверны.
Ко всему прочему, мы до сих пор не могём разрешить нелинейных дифференциальных уравнений в системе с парой десятков неизвестных (читай, энергетически оптимальный запуск ракеты), что уж говорить про тензорную и топологическую ересь.
А то что Гёдель доказал вам стоит почитать ещё раз, математика не может ошибаться если она непротиворечива, но при этом может быть неполна (т.е. какие-то истинные утверждения могут быть невыводимы, но это цена за точность), а вот если полна, то может ошибаться, но такой вариант видимо на практике бесполезен.
Нам предстояло разработать технологию совместных испытаний двух «изделий в целом» после их стыковки и весь многоступенчатый технологический план работ на стартовой позиции. Эту работу Королёв поручил молодому заместителю Воскресенского Евгению Шабарову. Почему не самому Воскресенскому? Здесь в который раз я убедился в умении Королёва выбирать людей для соответствующей задачи.
Воскресенский был испытатель высшего класса, одаренный необычайной интуицией. Кто-то метко его охарактеризовал: если бы он был лётчиком, то рисковал бы, как Чкалов. В отношениях с атомщиками партизанские действия были абсолютно недопустимы. Кроме существа дела, требовалась и его чёткая, последовательная формализация.
Что будет, если при подготовке ракета с атомной бомбой свалится у старта по причине, аналогичной упомянутому выше разгильдяйству с незакрытым баком перманганата натрия? Методика работы атомщиков предусматривала тройной контроль всех операций по сборке и испытаниям. Руководитель сборки или испытаний держит инструкцию и слушает, как испытатель громко читает содержание операции, например: «Отвернуть пять болтов, крепящие крышку такую-то». Исполнитель отворачивает. Третий участник работ докладывает: «Пять таких-то болтов отвернуты». Контролёр — представитель военной приемки — докладывает, что выполнение операции принял. Об этом делается роспись в соответствующем документе. Только после этого вся компания может переходить к следующей операции. Работа идет медленно, скрупулёзно, с обязательной громкой читкой, обязательным громким докладом об исполнении и распиской в особом технологическом журнале.
У нас таких строгих формальностей не было. Когда Шабаров обо всей этой методике рассказал Королёву, тот решил, что там, где мы будем работать вместе, надо «им показать, что мы не хуже». Ну, а что касалось нашей собственной деятельности, то для ракеты Р-5М необходимо было пересмотреть все инструкции по подготовке на технической и стартовой позициях и тоже ввести тройной контроль: основной исполнитель — воинская часть (офицер или солдат), контролирует офицер — специалист соответствующего управления полигона и обязательно представитель промышленности.
Так что и раньше в принципе можно было резко снизить брак и глюки в критически важных местах, но видно же, какое это мучение, как это долго и экономически невыгодно. Нужна некая золотая середина.
Другое дело — что если, как worldmind пишет, удастся сделать технические средства для устранения багов в коде и железе математическим путём и, разработав эту систему 1 раз, дальше можно будет использовать без затрат — это было бы неплохо.
Глючность это преимущество.
Эволюция — выживают сильнейшие.Известное заблуждение: на самом деле суть в размножении. Биология поведения человека. Лекция #2. Эволюция поведения, I [Роберт Сапольски, 2010. Стэнфорд].
Лучше написать глючную, но полезную программу, чем написать хорошую бесполезную. В принципе и бизнес так думает.
Было бы кому-то нужно написали бы идеальные программы. В математике (!), о которой идет речь строгих доказательств до 20 века не было. Эйлер суммировал расходящиеся ряды, Рамануджан большинство формул выводил методом приближений и иногда даже не доказывал, а уважаемый Ферма по всем решениям оставлял заметки на полях, с одной, правда, задачей плохо получилось.
Не пытаюсь никого переспорить, математика не формализировалась, пока это не стало нужно. Сейчас программы работают относительно стабильно, а ошибки быстро исправляются, зачем формальные доказательства?
кто уверен что вирус не начнёт ядерную войну?
Ядерная война,
Ядерная война,
Кто мне расскажет, кто подскажет,
Скоро ли она?
хм. а что вы думаете по поводу заявлений о том, что текущего ядерного запаса хватит на то, чтобы уничтожить землю n колличество раз?
Собственно, уничтожить землю буквально, как в «лекксе», по моему невозможно в принципе — грав. энергия связи слишком большая, первая космическая скорость соответствует температуре в порядка сотни тысяч градусов. Т.е. ее сначала нужно расплавить и испарить, а потому уже она начнет убывать в космос.
при ядерном взрыве загрязнение начинается Плутонием-239 и Ураном-235. Загуглите их активность, тысячекратно выше
Бред. При взрыве атомного боеприпаса (хоть уранового, хоть плутониевого) загрязнение обуславливается осколками деления исходного материала боеприпаса.
Сам по себе уран-235 практически не радиоактивен, его период полураспада составляет порядка 10^8 лет. Это красноречиво говорит о его активности. У плутония-293 период полураспада 24000 лет, активность повыше, конечно. Давайте попробуем прикинуть величину загрязнения, если предположить, что плутониевый заряд не взорвался, а просто равномерно распылился по территории вследствие взрыва обычного ВВ (аналог «грязной бомбы»). Считаем:
Дано: активность одного грамма плутония-239 — 2,3ГБк, масса боезаряда порядка 50 кг, распыление происходит на круг диаметром 5 км.
Пересчитаю активность из беккерелей в кюри, получу активность грамма плутония 62мКu, активность всего боезаряда — 3108Кu. Площадь круга радиусом 5 км составит 78,5 кв.км. На каждый квадратный метр при этом придется активность порядка 40 мкКu, или примерно 1,5МБк. Это много. Но зиверт за минуту не набрать.
Но, повторюсь, загрязнение после взрыва атомного боеприпаса осуществляется не исходным изотопом — он практически полностью распался, а осколками деления, которые действительно, очень радиоактивны на несколько порядков выше своих родительских изотопов.
зиверт за минуту не набрать
Ну если посчитать и другие радионуклиды в центре взрыва, то можно и поспорить. В любом случае я хотел показать, что при ядерном взрыве заражение гораздо более серьёзное, чем при аварии на АЭС.
Дано — реактор ВВЭР-1000. Масса топлива в одном ТВЭл — 1,565 кг. В тепловыделяющей сборке (ТВС) 312 ТВЭл, в активной зоне 163 ТВС. Итого общая масса топлива в активной зоне составит 79589 кг. Так как обогащение топлива у ВВЭР-1000 составляет от 3,3 до 4,4 процента (возьмем в среднем за 4 процента), то масса чистого U-235 составит 3183 кг. Предположим, что выгорание составило 50%, то есть, распалась половина массы U-235 — все атомы в 1590 кг урана распались на осколки (крайне радиоактивные, как я уже говорил).
Теперь сравниваем это массу радиоактивных веществ с массой радиоактивных веществ, образовавшихся при делении всех атомов U-235 в 100 кг атомного боеприпаса.
Итак, при тепловом (неатомном) взрыве на АЭС и произошедшем вследствие этого распределении топлива по территории загрязнение в 15 раз превысит аналогичное загрязнение от взрыва атомного боеприпаса.
Конечно, это некорректное сравнение в плане того. что мы не учитываем другие поражающие факторы атомного взрыва — ЭМИ, нейтронный поток, световое излучение, ударная волна. Плюс, естественно, при атомном взрыве радиоактивные вещества будут разбросаны на бОльшее расстояние, чем при тепловом взрыве на АЭС. По совокупности поражающих факторов ущерб от атомного взрыва, скорее всего, будет превосходить ущерб от теплового взрыва на АЭС.
Но если говорить только о загрязнении, то в последнем случае загрязнение будет значительно выше (чисто по массе РВ — в 15 раз), плюс распределится это загрязнение на меньшую площадь, а значит, удельное загрязнение на единицу площади будет еще больше.
Погуглите, что такое «наведенная активность», если не верите мне.
Вот нашел с ходу:
А это цитата оттуда:
Например, нежелательно содержание в таких сплавах никеля, молибдена, ниобия, серебра, висмута: они при облучении нейтронами дают изотопы с длительным временем жизни, например 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 лет. Тоже немало на самом деле.
Идея не пережила коммерциализацию, в связи с крайне высоким уровнем сложности реализации для сколько-то сложных программ. На данный момент впрочем, в связи с ростом связности систем, интерес к концепции по немногу возрождается.
Просто статьи про функционально безопасное ПО зачастую очень общи, содержат пространные рассуждения, много воды. И эта статья не исключение.
А вот если приземлённо, без теоретизирования: объясните программистам пишущим софт для управления железнодорожной станцией — как они должны его писать?
Чтобы рассуждения не были опять-таки отвлеченными, пусть структура системы будет такой:
1. Т.н. напольное оборудование (стрелки, сигналы, рельсовые цепи, ну и всякое по-мелочи).
2. Шкаф управления напольным оборудованием обеспечивает безопасную увязку с п.1. Функционально безопасную. Т.е. объекты будут изменять состояние только по командам и никак не самопроизвольно, сигнализация от объектов будет поступать корректная, однозначно соответствующая их реальному состоянию. Это, вообще говоря, тоже не тривиальная задача.
3. Центральный Вычислительный Комплекс (ЦВК).
4. АРМ пользователя. Собственно он не обязан быть безопасным. Вся безопасность заключается в ЦВК.
ЦВК это, к примеру, трёхканальная система, работающая по мажоритарному принципу (2-из-3). Если один канал начинает выдавать данные, не совпадающие с остальными двумя — он отключается и система начинает «хромать» по принципу 2-из-2: ЦВК управляет только пока выходные данные обоих оставшихся комплектов совпадают. Возможно с урезанием функционала.
Если же начинают расходиться данные оставшихся комплектов — система переходит в защитное состояние до вмешательства обслуживающего персонала.
Чисто алгоритмически, ЦВК выполняет увязку стрелок, сигналов и рельсовых цепей так, чтобы не допустить враждебностей и опасных воздействий на подвижной состав (перевод стрелки под составом, некорректное перекрытие сигнала перед поездом).
Ну и, понятно, нужно обеспечить пропуск поездов по станции с требуемой интенсивностью.
Как к данной задаче применить упомянутый Вами метод создания ПО?
Без теоретизирования математическую теорию никак не объяснить, но тут в комментах говорят о знакомстве с теми, кто занимается формальной верификации, можете попробовать напросится на лекцию.
Писать-то можно также, а вот проверять по другому
Как же «также»?
И как доказать, что в программе нет зависимости состояния сигнала в одной горловине от положения стрелки — в другой? Кроме нормативного конечно.
Полным перебором всех комбинаций всех значений всех сигналов и переменных со всеми временнЫми выдержками? (время — это тоже параметр)
Другое дело, если говорить о микропрограммах для жизненно важного оборудования, вот там да, стоимость бага сильно велика и конечно этому стоило бы уделять побольше внимания, возможно даже и на мировом уровне, вот только, что делать с «загребущими руками»? Если начинать вливать в эту отрасли большие деньги на зарплату, то сразу найдутся люди, которые просто будут нахлебниками и средний интеллект в такой команде не увеличится. Да, через пару тройку лет возможно и получится отсеять некоторых недобросовестных людей, но за это время добросовестные задолбутся получать по шапке за тех, кто криво делает. Наказания спросите вы? А что стоит наказания одного раздолбая, если выпущеный серийный аппарат МРТ, например, поджарит пару десятков человек?
Ну дальше я не буду развивать эту тему, наверно стало немного понятно, что хорошее оборудование с малой вероятностью появления багов стоит очень дорого и не из-за того, что там работают дорогостоящие сотрудники и загребают деньги лопатой, а из-за того, что весь этот процесс очень и очень сложно организовать из-за человеческой натуры.
Ровно из-за этого на наше с вами баловство с ПК ни кто не будет писать софт без багов.
если выпущеный серийный аппарат МРТ, например, поджарит пару десятков человек
Серийно выпускаемые автомобили убивают около 3500 человек в мире каждый день. Многим это не нравится, но от автомобилей никто избавляться не спешит.
Эту проблему надо решать по другому. А вот небольшой наброс на вентилятор: представь теперь, что писать код для него будет тот человек, которому этот аппарат необходим, какова вероятность того, что он халатно отнесётся к написанию программы?
А неважно насколько халатно человек отнесётся, человек при всём своём желании не может быть безошибочным, одни когнитивные искажения чего стоят, а есть куча других факторов (не доспал, простыл, отвлекли, не сообразил, забыл...) из-за которых даже самый ответственный человек может ошибиться.
Человек не надёжное звено в любом случае, каким бы он ни был.
Работой по формулировке алгоритма математического доказательства в течение четырех лет занималась команда из 12 исследователей NICTA, аспирантов и техников. Они успешно проверили более 10 тыс. промежуточных теорем, изучив более чем 200 тыс. строк кода. Итоговый анализ выполняется с помощью интерактивной программы Isabelle, и на сегодняшний день является самой объемной автоматизированной проверкой выполнения условий теорем.
Наряду с доказательством соответствия программного кода выполняемым функциям, тестирование показало, что seL4 не подвержен большинству известных хакерских атак. Например, атака «переполнение буфера», позволяющая внедрить злонамеренный код и захватить управление работой ядром, не даст результата.»
Примерно миллион долларов и человечество получило микроядро беспрецедентной надёжности, доступное всем по свободной лицензии.
Уязвимости да действительно появляются из-за человеческой невнимательности. А вот проблемы в бизнес логике, чаще появляются из-за проблема коммуникации между людьми. Программист их намеренно делает думая, что так и надо.
Тут же возникает вопрос о специалистах которые хорошо шарят не только в программировании но и в области той науки для которой он пишет софт, а это очень часто редкие люди. возможно стоит пойти дальше и пересмотреть подготовку специалистов, убив еще 2-3 десятка лет.
В любом случае верификация кода на очень быстро развивающихся железках (я не говорю о баловстве с ПК) — это очень проблематично.
2. Проблема с корректностью требований не решается верификацией, это я отметил, но с требованиями проблемы в бизнесе, а в медицине, авиации, космосе, АЭС требования вынуждены формулировать максимально точно (иначе оно бы и не работало).
3. Да, специалисты нужны другого уровня, не обезъянокодеры, а математики-программисты. Да, нужно начинать их готовить, если этого не делать, то так и будем терять космические аппараты с бешеной стоимостью из-за программных ошибок, проводить некорректные исследования из-за багов в МРТ и т.п.
>> В новую версию принято более 13 тысяч исправлений от примерно 1500 разработчиков, размер патча — 41 Мб (изменения затронули 11303 файлов, добавлено 627751 строк кода, удалено 278958 строк).
вопрос: сколько людей и сколько времени будет проходить верификация только нового кода?
8700 строк кода — 12 человек — 4 года
348793 новых строк кода — ? человек — ? лет
дополнительно учитываем, что сложность верификации совсем нелинейна относительно объема кода (лично я допускаю что ближе к экспоненте)
Да, многие вещи в ядре дублируются и тд, тех же fs вагон и маленькая тележка, но все они кому-то нужны, так как специализированны под конкретные требования, нельзя написать одну fs которая удовлетворит всех, а потом её верифицировать и все счастливые.
p.s. сам регулярно прогоняю статический анализ по своему код, но это далеко не верификация, так как она будет не просто дорого, а очень дорого, проще переписать 10 раз с нуля под изменившиеся требования, чем 10 лет пилить морально устаревшее решение
верифицированный L4 это по сути минимальный гипервизор, который почти ничего не умеет.
В самом linux kernel от ядра как таковое совсем малый процент
первое место по объему это драйвера
дальше уже arch (все-таки количество поддерживаемых архитектур зашкаливает, сравните с seL4 который 4 вида arm и одни ia32 тянет)
и третье место за fs.
то есть формализовать только какой-то subset от ядра не проблема даже для монолита.
а вот формализовать все ядро действительно нету шансов
к тому же если посмотрите на последние уязвимости-ошибки, то окажется что по отдельности они не несут никаких деструктивных вещей, зачастую это даже ожидаемое их поведение, но вот грамотное построение цепочек из 10-15 таких недоуязвимостей создают большую дыру и тут даже верификация и микроядро не поможет, так как каждое из действий будет считаться допустимым, а истинная проблема возникнет на стыковке и объединении всех модулей
Но конечно в сфере о которой я говорю не будет такого зоопарка архитектур, ФС или устройств.
и вот тут мы начинаем спускаться уже глубже:
ядро для os для атомных, космических и медицинских вещей и так далеко не обычное используется, говорить, что там меньше архитектур и fs я бы точно не стал, так как хватает всего, поэтому и разработки такие дорогие, что продукты очень часто близки к уникальным или тираж очень маленький.
«а всё остальное на условном кроссплатформенном хаскеле нужно писать» — все любят повторять это как мантру, раз математический язык, то все хорошо, но почему-то все забывают уточнять, что как только поменялась немного модель данных, то с хаскелем все очень весело становится, про разворачивание ошибок компиляции отдельный вопрос (это все вытекает из математики).
иногда проще поступить по принципу эрланга: если что-то падает, дай ему упасть.
Но в нашем случае продолжаем работать и принимать решения уже на оставшихся данных, так как любая физическая сущность всегда может упасть или начать возвращать неправильные данные (можете посмотреть количество сбоев обычной RAM в датацентрах, интересная статистика, посмотрите на последние уязвимости Rowhammer), то есть ваша программа формально будет вести себя правильно, но данные ей будут поступать некорректные.
А есть что почитать про медленно компилирующий верифицированный компилятор?
Верифицировать схему не особо сложно. Сложно верифицировать ситуацию «в этом куске кремния нет неучтенных эффектов». Вам же его и производить прийдется на верифицированном оборудовании. Сейчас при запуске очередного техпроцесса уходят месяцы подтасовок оборудования(называемых «наладка техпроцесса»), в случае верификации вы должны ее заново начинать после любого минимального изменения неучтенного в предыдущих теоремах.
компилятор тогда быстрее будет — не будет заниматься оптимизацией
Считается, что квалифицированный программист может выдавать 200 строк качественного, оттестированного кода в день. Таким образом, 8700 строк было бы написано 1 программистом за, примерно, 2 месяца (с учетом выходных).
Получается, что потрачено 2 человеко-месяца на разработку и 576 человеко-месяцев на тестирование.
На этом дискуссию можно заканчивать. Такое делается 1 раз с целью показать: «вот, смотрите, как мы можем», — но в реальной жизни это неприменимо. Хотя бы потому, что не существует необходимого количества «исследователей».
квалифицированный программист может выдавать 200 строк качественного, оттестированного кода в день
Хрень полнейшая! Вы — индийский менеджер на индусскими программистами?
Всё зависит от задачи — можно, и две строчки за весь день выдать, если ищешь ошибку среди десятка тысяч строк, а можно и две тысячи строк за день накатать, если задача простая и ясная.
или его появление в 10 клиниках в мире через 20 лет за цену 1000*X
я выбираю первый вариант, так как в некоторых случаях это нужно здесь и сейчас, а не через год, не говоря уже о больших сроках. многие новые разработки являются уникальными, либо используют новые физ-мат модели и переиспользовать просто нечего, поэтому фраза оказывается ложной:
>> Заоблачной стоимость будет только если каждый производитель каждый раз будет заново писать и верифицировать весь свой код, а если будут использованы ранее верифицированные открытые компоненты, то стоимость вырастет не сильно.
даже с обычной жизни мы постоянно сталкиваемся с вероятностями в медицине:
экспресс тесты на беременность/ВИЧ/диабет.
Не будет такого выбора.
Речь не о том, чтобы остановится в развитии, а о том, что надо двигаться в правильном направлении, вот есть у нас теперь верифицированное микроядро, значит стоит использовать его в новых МРТ, а не костылить что-то своё, появится следующий верифицированный компонент (например ФС), значит новое нужно делать используя его.
Не будет такого выбора.
Речь не о том, чтобы остановится в развитии, а о том, что надо двигаться в правильном направлении, вот есть у нас теперь верифицированное микроядро, значит стоит использовать его в новых МРТ, а не костылить что-то своё, появится следующий верифицированный компонент (например ФС), значит новое нужно делать используя его.
Вы уже 10 раз это написали. Дайте пруф, что это так. И с чего вы взяли, что я, потратив очередные 48 человеко-лет на верификацию своего компонента (например ФС), разрешу вам использовать его бесплатно? Цена в 1000*Х это, на мой взгляд, даже оптимистичный прогноз.
Это конечно один пример, но тут ситуация как с линуксом — каждому в одиночку такое пилить слишком дорого, поэтому компании-конкуренты скидываются и пилят ядро вместе, а защитой для них является GPL.
Это конечно один пример
Это пример того, как по приколу напряглись и показали как подход можно применить для микроштуки, угробив, как минимум, в 50 раз больше ресурсов, чем требовалось.
Дайте расчет или пример того, сколько придется угробить ресурсов для десятка миллионов строк кода. Только не надо сказок про то, что мы сделает 100500 финтифлюшек, протестируем каждую и это будет гарантировать, что все вместе они заработают как надо. Не позорьтесь.
Я вроде пояснил уже, что если верифицированные компоненты будут создаваться не в рамках конкретных продуктов, а параллельно, то они не будут замедлять их развитие, и не сильно будут увеличивать стоимость т.к. затраты будут распределяться по большому количеству продуктов в которых они используются.
Так, например, весьма большая стоимость свободных дистрибутивов не приводит к дороговизне домашних роутеров построенных на них.
А ещё вспомним, что раньше, в 19 веке, среди инженеров — мостостроителей, было принято становиться на лодке под построенным мостом, когда по нему пускали первую нагрузку (поезда, телеги).
Так вот, ежели заставить разработчиков софта для МРТ и авионики на себе испытывать эти установки, ответственность сама по себе возрастёт (никто не захочет умереть от своего изделия).
То есть, банально восстановим принцип персональной ответственности инженеров за свои изделия.
Жарить с помощью МРТ сложно, но магнитные поля очень сильные: 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."
http://medicalphysicsweb.org/cws/article/opinion/48264 Jan 10, 2012 MRI safety: accidents are not inevitable
FDA's medical device accident database, MAUDE… showed that reported MRI accidents in the US have risen over 500% from 2000 to 2009. During that same time period, according to market research firm IMV, the overall number of administered MRI exams increased by approximately 90%.… three categories: burns, projectiles and hearing damage.… burns caused by electrically conductive materials in the bore with the patient; burns caused by proximity to/contact with active RF elements; and resistance to electrical currents generated in the patient's own body as a result of large calibre tissue loops. ..
http://cds.ismrm.org/protected/09MProceedings/files/Fri%20A18_08%20Sawyer.pdf "Burns from RF Electromagnetic Fields ..."
Был еще такой одиночный случай в Индии из-за магнитного поля: http://www.dailymail.co.uk/news/article-2890088/Two-hospital-workers-spend-FOUR-HOURS-pinned-MRI-machine-metal-oxygen-tank-catapulted-room-device-s-giant-magnet-turned-on.html — "Two hospital workers… pinned to MRI machine by metal oxygen tank… India … Normally the incident could have been over within seconds, but the machine's emergency shut-off switch failed to work… Later reports suggested the switch had been disabled so it could only be operated by GE employees. A GE spokesman declined to confirm or deny that"
Кнопка экстренного "размагничивания" не отключила магниты по неясным причинам. Известно, что аварийный останов может потребовать длительного ремонта и замены газов на десятки тысяч долларов: http://www.auntminnie.com/index.aspx?sec=ser&sub=def&pag=dis&ItemID=110120 "magnet rundown units (MRUs), which are designed to initiate a controlled quench and turn off the magnetic field… Such shutdowns are only intended for extreme emergencies and can put an MRI magnet out of commission for a week or more and cost up to $30,000 to replace lost helium"
Последовал отзыв и доработка: http://www.auntminnie.com/index.aspx?sec=ser&sub=def&pag=dis&ItemID=110120 "In GE's case, a scanner's magnetic rundown unit may not actually be connected to the scanner, according to the FDA recall notice.… MRI scanners in India had been modified by service personnel or by equipment users to disable the magnet rundown unit"
Безумные эксперименты со списанным МРТ — https://www.youtube.com/watch?v=6BBx8BwLhqg (крупные железные предметы), https://www.youtube.com/watch?v=9SOUJP5dFEg (quench, при котором выкипает жидкий гелий)
А что стоит наказания одного раздолбая, если выпущеный серийный аппарат МРТ, например, поджарит пару десятков человек?
Такое уже было, мне известен как минимум один прецедент (правда не мрт конкретно, но суть та же)
При УЗИ беременных сканер Тошиба SSA-660 мог пережаривать плод:
"Локальное увеличение температуры пациента… не показывалось из-за ошибки в ПО".
http://webcache.googleusercontent.com/search?q=cache:7rJ0CGtgQmsJ:https://www.swissmedic.ch/recalllists_dl/00278/Vk_20060104_06-e2.pdf%2Blocal+increase+patient+temperature
"not displayed even if the value is 0.4 or more in 2D mode (B mode) due to a software error."
2) на хабре кто-то в комментариях писал про своего знакомого московского главного админа процессингового центра банка. Который сразу же снимал наличку со своей пластиковой карты в день зарплаты, видимо ожидая прилёта разрушительных "дятлов" с минуты на минуту :)
3) Тут же в блоге мегафона написано про их страх насчёт облысения от СВЧ в собственных тестовых экранированных комнатах.
4) анекдот: "С тех пор, как я начал водить машину, я стал осторожнее переходить дорогу."
Думаю, для того чтобы земная цивилизация устойчиво развивалась
Думаю, что прежде, чем вносить какие-то предложения по устойчивому развитию, было бы неплохо обосновать смысл и пользу именно устойчивого развития по сравнению с альтернативами. А то этот термин стал нарицательным и вобрал в себя всю палитру оттенков ретроградства, бессмысленной перестраховки и, как итог, тотальной неэффективности.
Можно конечно вернуться в каменный век для надёжности, а можно сделать технологии лежащие в основе интернета столь надёжными чтобы никакие хакеры не могли остановить жизнь цивилизации.
1) трактористы Васи порвали экскаватором оптику (реальный случай пропадания аплинка между РБ и Россией, в тот момент там свыше 50% всего внешнего канала было, сколько рвут кабелей океанических вообще помолчим).
2) ударили молнии и вторая половина датацентров легла (случай с амазоном)
Распределенные технологии, такие как интернет, по определению строятся на ненадежных системах, чем больше узлов в системе тем выше вероятность отказа. Поэтому для интернета стоит задача другая: как из ненадежных элементов построить достаточно устойчивую систему. Отмирание отдельной клетки не убивает организм (рак отдельная песня, но и с ним частично борются), выпадение одного сервера не ложит yandex/google/facebook (для них вылеты целиком стоек никак не сказываются на работе, даже падение целого датацентра не остановит работу). Те же DDoS это полностью правильная работа, но датацентр можно положить, тут не спасет никакая верификация.
Поэтому отдельные части верифицировать можно, но чем крупнее система, тем больше нужно полагаться на общую устойчивость, а не на то, что у нас каждый элемент будет работать правильно и идеально и никогда не сбоить.
Shubinpavel уже вам ответил за космос: проблема зачастую в ресурсах (время, деньги, человеки) когда сознательно идут на срезание улов и уход от поставленных требований к проверке надежности, но чтобы было хоть что-то, а не воздушные замки в мечтах.
NASA имеет бюджет, любой спутник или ракета имеет бюджет, поэтому иногда возможно рискнуть и попытаться запустить сейчас с вероятностью неудачи в 0.001% чем пропустить запуск и ждать следующих 4-5 лет для появления окна запуска. В случае неудачи у вас есть риск строить такой же аппарат еще 8 лет, но это сознательный риск.
Не задумывались почему даже на Curiosity обновление прошивки заливали уже после достижения Марса: в момент отправки оно просто не было готово, не хватает ресурсов.
Простейшая, даже самая очевидная программа — X = A + B где A и B — целые 32-битные числа. Количество вариантов которое надо проверить чтобы выдать положительный вердикт — 2^64 степени, при вычислительной мощности процессора 1000МFLOPS время на тест такой простейшей программы полным перебором составит не менее 18446744073 секунд, или почти 585 лет непрерывной работы. И это для простейшей очевидной программы, работоспособность которой легко доказать.
И по-моему Вы упускаете один аспект или как вы их называете причину, как насчет того что человек в силу своей несовершенности не может учесть всего? Взять ту же АЭС, сможете перечислить все возможные варианты событий, которые могут произойти и которые надо учесть в ПО? Мы в обычной жизни не всегда можем все варианты просчитать, что уж говорить о сколько-нибудь серьезных проектах. И тут уже проблема не в глючности, а именно в том что все это для начала учесть, а потом и запрограммировать, а потом еще и проверить.
А корректность самих «проверяльщиков» (будь то ПО или люди) как проверить?
Почему проверенная ими программа будет более корректной если мы не можем доверять проверяльщикам?
Допустим, надо вычислить высоту над поверхностью. Расчёт высоты ведётся не одной подпрограммой, а тремя одновременно, но три подпрограммы разные по алгоритму и писались разными программистами. Если объёмы устройств позволяют, то компьютеров физически три. Управляющее устройство срабатывает, если от двух и более алгоритмов поступили одинаковые цифры.
и тоже был какой-то инцидент
Ну или не «ди», а N.
Мы просто разрешаем существовать только гарантированно выполнимым функциям. Проворачивается это каким-нибудь таким способом:
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, но и доказательство того, что у переданного значения вес меньше, чем у предыдущего. Тогда, очевидно, рекурсия не сможет продолжаться бесконечно, т.к. когда-нибудь она упрётся в нижнюю границу.
И все наши программы будут завершаться когда-нибудь (если никто не будет вычислять что-нибудь невероятно долгое, вроде функций Аккермана — ограничивать по времени выполнения куда сложнее, придётся описывать виртуальную машину и ограничивать количество выполняемых инструкций).
Первый путь будет означать, что желая создать функцию
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-комбинатором те же дела, это просто обобщённая функция, тип которой является запрещённым рекурсивным.
у меня есть правила, какие типы разрешены, а какие нет, но не буду их здесь описывать, если нужно — спрашивайте
А какие правила помимо того, что тип не должен стоять в отрицательной позиции?
Тип X предоставляет A если:
- Равен A.
- Является произведением типов, один из членов которого предоставляет A.
- Является суммой типов, все из членов которой предоставляют A.
- Возвращаемое значение функции предоставляет A.
И вот в описании типа A типы, предоставляющие A не могут быть использованы в качестве типа аргумента функций внутри этого типа.
- Ограничили типы `T = T → 0`
- Ограничили типы `T = (T, AnyOtherTypes) → 0`
- Ограничили типы `T = (T + (T, AnyOtherTypes)) → 0`
- Ограничили типы `T = (Unit → (T + (T, AnyOtherTypes))) → 0`
Но ситуация усложняется, когда мы начинаем задавать группу рекурсивных типов. Например, что-нибудь такое:
A = B + C
B = 1 + C
C = 1 + B
Не знаю, можно ли как-то сворачивать их в один тип, не выглядит тривиальным, поэтому я просто расширил правила с рекуррентностями на такие группы и там получается матрица рекуррентностей, где каждый из типов имеет флаги, предоставляет ли он значения остальных типов (включая себя).
Но в природе существуют программы биороботов, веками не устаревающих и без побочных эффектов.
«Верный мотив – работа на Общее Благо и Служение Жизни.
Неверный мотив – всё, что заставляет вас преследовать любые цели, принадлежащие физическому плану: слава, деньги, почёт, получение удовольствий, удовлетворение желаний.»
Важно понять, что смысл не в том, чтобы избавиться от всех дефектов, а в том, чтобы найти какой-то подход, который позволит избавиться от многих дефектов минимальными усилиями с учетом современных реалий. Формальная верификация тут не пройдет.
Другими словами, наличие тестов не может поменять суть надежности, как вероятностной оценки, на что-то иное.
Формальная верификация берёт два документа — текст программы и требования, записанные на некотором логическом языке, и доказывает их эквивалентность.
Проблема в том, что для сложных систем написание требований — то же программирование, где можно допустить тонны опечаток и ошибок.
По моему опыту, на Прологе можно сажать больше ошибок на строчку кода (концентрация нужна выше, и привычка). А спецификация, по сути, что-то типа Пролог-программы.
Казалось бы, двойная проверка. Но, чтобы программа «сошлась» с описанием, программист в случае проблем проконсультируется с составителем правил (если это не одно и то же лицо), и спросит, почему его программа не проходит проверку. Или тупо скопипастит логику из правил, подправит программу под спецификацию. А что если, он не так трактовал какое-то требование, как составитель спецификации (а на самом деле его трактовка была изначально правильной). В итоге, неверные допущения, когнитивные искажения, заблуждения проникнут и в требования, и в программу.
И, казалось бы, верифицированная программа, но глючить она тоже будет.
А вот математически корректные программы — баба Яга против. Завтра мне может понадобиться взять в руки дебаггер чтобы остановить какое нибудь зарвавшееся сборище бизнесменов, программистов и инопланетян — а с такими программами это будет бесполезно.
За спиной раздался грохот, небо разом потухло, профессора швырнуло вперед на микрофонную стойку, и наступила темнота…
Итак, хоминоиды — Леонид Каганов
Её просто не проверяют. Ко мне приходит заявка (устно, письменно — не важно), я проверяю входные данные, у меня есть факт на выходе и то, что должно было получиться на выходе по идеи. Исправляю программу, отдаю. Далее автор заявки убеждается в том, что при тех данных, которые он подал на входе утром он получает правильный выход и закрывает заявку, но не проверяет ни предыдущие месяцы, ни другие комбинации различных настроек. В следующем месяце, с новыми данными и настройками, примерно 50-на-50, что результат будет некорректен и у меня появится очередная заявка от того же автора. И можно всю жизнь просидеть на такой техподдержке.
Примерно также то и дело прилетают заявки от людей, которые работают с передачей данных в смежные системы (или с получением данных от них), а общее количество систем, с которыми идет обмен данными, постоянно растет и уже превышает дюжину. Исправляем, проверяем этот месяц, ждем заявку в следующем месяце. Говнокод как он есть.
В порядке шутки: новости дня «Сегодня [недалёкое светлое(?1) будущее], в 16-00 смыло деревню Гадюкино со всем населением. Наши информационные источники сообщают — причиной катастрофы была ошибка математической теоремы в программах местного Гидромета. Напомним, на прошлой неделе, из за аналогичных причин аппараты Breakthrough Starshot промазали мимо a-Центавра».
Люди говнокодят, но проблема не в людях, а в природе, которая тоже даёт баги. Вся мутация — это эксперименты между — прокатиться и выжил, или непрокатило — умер.
Ответ на все эти вопросы один, этот инструмент — математика
Которая тоже не совершенна на текущем уровне
Так вот создать что-то быстро, дешево и качественно это утопия. Полное математическое покрытие тестами продукта? Чем больше в нём зависимостей, тем сильнее растет количество необходимых тестов. Так что людям приходится находить компромиссы.
http://bodunov.org/images/stories/SC_Software.pdf
Да, есть стандарты на ПО в системах ответственного применения. Но сказать, что проблема состоит лишь в том, что плохие разработчики не желают следовать этим стандартам — это слишком смело. Потому что надо проверять сами стандарты, и самих проверятелей… и так до бесконечности. Еще римляне выразили всю сложность проблемы в фразе «Кто будет сторожить сторожей?»
Формальная верификация — это очень круто и интересно. Мне бы очень хотелось работать в данной области. Но факт в том, что это никому не нужно. И вряд ли это станет мейнстримом в ближайшем будущем. Грусный смайлик.
Apple, Intel (там ещё горстка других вакансий у них же), NXP, ARM.
И софтварные вакансии тоже иногда появляются, я уверен. И нужно быть готовым к такой, ибо ты не скажешь «ребята, у вас крутая вакансия, подождите, я тут три года попрактикуюсь и сразу к вам».
Деньгами, что Вы мне обещали, пиво собеседнику оплатите, если есть желание пообщаться в Москве :)
Это могу только посоветовать нагуглить на ВМК МГУ + Ваш запрос. Там этим занимаются, причем студенты — в обязательном порядке :)
Гуглите, списывайтесь с кафедрой системного программирования, а у них запросов на этот счет хватает, сведут Вас с интересными людьми. Там как раз стонут, что всем только базы данных нужны :)
Может кому интересно почитать будет, есть такая книжка — Стивен Спир "Догнать зайца". Там рассматривается в том числе практика устранения косяков в медучреждениях США и на флоте.
Вот, собственно, так все и работает :)
Почему земляне делают глючный софт и железо