незваный гость писал(а):
Я готов оспорить абсолютно любое утверждение, просто заявив что то, на чём оно основано не абсолютно истинно.
И не собираюсь кому-то что-то доказывать. Почему-то вы считаете, что результатом обсуждения должно быть 2 человека с одним мнением по обсуждаемому вопросу. Я так не считаю.
незваный гость писал(а):
Ваша же аргументация против моих тезисов, на мой взгляд, слаба. Может быть, Вы просто не поняли меня (я не мастер выражаться), но…
У меня нет аргументации "против тезисов". У меня есть мнение, которое не такое, как ваше. Оно не ставится в позицию "категорически против".
незваный гость писал(а):
Между тем, математическое доказательство абсолютно: если в нем есть ошибка, то результатом пользоваться нельзя.
Почему нельзя?
Повторяюсь в третий раз: доказательство правильности не доказывает отсутствия ошибок (меня с
bak'ом путать не надо). Оно занимается поиском ошибок (это в случае верификации готового ПО) либо помогает строить ПО с меньшим уровнем ошибок (использование доказательства правильности во время создания ПО или до). В любом случае это инструмент, которой позволяет улучшить качество ПО. И если даже док-во правильности не нашло ошибок, это говорит о большей нашей уверенности в том, что ПО сделано более качественно.
незваный гость писал(а):
А вот теоремы существуют. Но главное, вопрос к Вам: готовы ли Вы согласится с этим утверждением?
Если я правильно все понял, то считаю это банальностью. Или определением. Того, что любое ПО работает на физическом носителе, то что имеет что-то дает ему что-то на вход и ждет на выходе, - все это можно определить как внешнее по отношению к ПО.
незваный гость писал(а):
Человечские жизни … деньги … Практичные янки при дворе президента Буша при разработке самолёта ориентируются на цену человеческой жизни порядка 300,000 $. Думаю, что у них есть и уставная единица для АЭС. Для компании (зачастую, небольшой), производящей кардистимуляторы, качество ПО — это вопрос жизни и смерти компании. Но слишком дорогое ПО — просто другой способ для компании умереть, будучи нерентабельной.
Да, я знаю что буржуи рассматривают человеческую жизнь в неком $-эквиваленте. Но у пост-советских стран другое отношение к системам, критичным к безопасности.
незваный гость писал(а):
Мораль: на данный момент я знаю (в силу своей ограниченности, несомненно) только один случай когда от программ требкется абсолютное качество: применение программ для доказательства математических фактов. Но мы, вроде, эти программы не рассматриваем.
Абсолютного качества не существует. И не только в ПО. Вы это написали первым же утверждением. Согласны?
незваный гость писал(а):
В какой-то момент музей становится перед выбором: покупать новую систему пожарной охраны, зная, что в её ПО есть ошибки, или жить со старой, зная, что в её механических/химических/… элементах есть дефекты.
Старая механическая система может быть построена на безопасных элементах (например реле 1-го класса). А если придет кто-то и скажет "Давайте я воткну микроконтроллер", то ему придется всем доказать, что это будет функционировать безопаснее старой системы. Иначе такое не пропустят туда, где предъявляются серьезные требования по безопасности функционирования.
незваный гость писал(а):
Вам, видимо, не хватает толики здорового цинизма. Если погибнет Мона Лиза, никто новой не напишет. Но музей получит вполне конкретную страховку. Страховая компания, в свою очередь, будет судить производителя пожарной системы. Тот укажет на свою страховую компанию, которая ущерб оплатит, но поднимет страховой взнос до небес. Так что “Money, money, money // Must be funny In the rich man’s world”. И, что самое любопытное, никто даже не вспомнит имя пождигателя. Я думаю, Вам понадобится немало порыться в Интернете чтобы найти имя морального урода (ой, по-моему теперь это борец за демократические идеалы), облившего Данаю кислотой. А прежнего полотна Рембранта нет. И не будет.
Вы не понимаете, что я пишу. Вопрос не в том, что произойдет. Вопрос в том, как строятся безопасные системы.
Всего лишь утверждение, что есть вещи, которые не оцениваются в $ . И для таких вещей нужно не деньги вкладывать, а использовать комплексные методы по снижению вероятности ошибок и сбоев, свЕдения всего этого к ничтожно малой вероятности проявления. И в таких случаях отказываться от методик доказательства правильности глупо, т.к. они позволяют эффективно находить такие ошибки, которые не выявляются никакими другими методами.
Если мона Лиза и Эйнштейн не понятны, то скажите пожалуйста, во сколько денег обойдется человечеству ошибка в ПО, которая запустит в ход атомную войну? 300,000 * 7 *
$ ?
Или можно сказать по-другому. Вы полетите на Марс в составе 1 из десяти ракет, каждая из которых долетит до Марса с вероятностью 20% ? Просто потому, что создатели решили особо не церемонится, и немножко сэкономить. Просто стоимость системы в силу описанного факта стала дороже на 3 млн $