Программа без ошибок - такая же абстракция, как -273 градуса

[незваный гость]

Ну-с, начнем по порядку.

bak писал(а):

Доказательное программирование - это составление алгоритмов и программ для ЭВМ с доказательством отсутствия в них ошибок.

Не похоже, чтобы структурное программирование чем-либо отличалось от этого определения. Я думаю, поэтому-то и нет отдельного термина на гнилом Западе. Зато и Дейкстра, и Грис, и Хоар (Hoar, C. Communicating Sequential Processes, 1978) использовали термин структурное именно в смысле доказательное. Термин нужен только чтобы свой несуществующий приоритет застолбить.

bak писал(а):

Спасибо за информацию об отсутствии исследований по "Доказательному программированию" на английском языке.

Я такого не говорил. Я говорил, что термина такого я не встречал. А исследования по доказательству (в том числе автоматическому) ведутся, и активно. Если Вы посмотрите сообщения Debiloid'а в этой теме, то увидите, что он успешно автоматически доказывал правильность программ в 10-15 тысяч строк (пишу по памяти). Но обычно автоматические системы доказательства правильности основаны на непроцедурных языках.

bak писал(а):

Программы без ошибок бывают. Они известны. Их можно найти в книгах и учебниках с доказательствами их правильности. Утверждающие обратное книг Э.Дийкстры и учебников по информатике не читали. Программ без ошибок не видели. Это плохо.

По-моему, плохо то, что эти программы известны. Лучше было бы, чтобы они назывались просто программами, а известны были бы программы с ошибками. А вот Ваша ссылка на учебники весьма смущает. Учебник -- это не серьезно. Это шутка. Во-первых, программа в учебнике в принципе не может быть большой. Серьезная программа -- это $10^4$ -- $10^7$ строк. Даже нижняя граница -- 170 страниц -- практически неприемлема для учебника. А для 10 строк другие законы. Во-вторых, "для упрощения", "понятности подачи материала" учебник выбирает хорошо поставленную и хорошо решаемую формулировку задачи. Идет намеренное абстрагирование от реальных условий функционирования программы. (За примером далеко ходить не надо. Сглаживающий фильтр Баттерворта первого порядка в любом учебнике будет написан в три строки (включая цикл). А Вы посмотрите на него в серьезной системе обработки сигналов. Если на страницу поместится -- хорошо. Про сортировку и вспоминать-то не хочется.) В-третьих, автор учебника не ограничен во времени на разработку своих программ. В реальной жизни программист работает в жестких временных рамках.

bak писал(а):

Сотрудники MS на своих конференциях прямо заявили, что доказательное программирование им не нужно.

Бог им судья. И Вильям Гейтс III, который им зарплату платит.

bak писал(а):

Лично у меня было шесть программных проектов, которые были сданы после 1-2 пуска на ЭВМ.

Мне очень нравится подход Д. Кнута, который установил экспоненциально растущий приз за ошибки, найденные в \TeX. За первую ошибку -- 1 цент, за вторую -- 2 цента, за третью -- 4. Выплатил за все вместе около 20 долларов -- не раззорился. Готовы ли Вы также встать за своими продуктами (не за учебными программами, разумеется)?

bak писал(а):

Отладка программ на ЕС ЭВМ носила в МИЭМ столь мучительный характер, что студентам-математикам было проще описать программы на псевдокоде с доказательствами их правильности. Тем более, что в 1983г. Администрация МИЭМ отказала всем студентам-математикам в пуске их учебных программ в ВЦ МИЭМ. Администрации МИЭМ - особая благодарность в переходе на технологию "доказательного программирования" - написания и анализа правильности программ без выхода на ЕС ЭВМ. Все студенты-математики писали и дрокументацию и доказательства правильности программ на родном русском языке, а программы на языках Fortran, PL/1, Basic, Pascal, C/C++.

При этом возникает интересный вопрос -- написали Вы программу на псевдокоде, доказали ее правильность, а дальше что? Откуда следует правильность трансляции псевдокода в реальный язык? Откуда следует правильность формализации интерфейса используемых в программе пакетов или библиотек?

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

bak писал(а):

Программы с доказательствами правильности можно писать на любом инструментальном языке программирования - Pascal, C/C++, Basic и т.п. Главное не в том - на каком языке пишутся программы, а какие алгормитмы реализуются в наших программах. "Алгоритмические ошибки" в программах - это ошибки, которые заложены в соответствующие алгоритмы.

Писать, разумеется, можно на любом языке. Можно объектно писать на ассемблере и неструктурно на Java. А вот удобно ли доказывать правильность программ на процедурно- ориентированных языках? Удобно ли автоматически доказывать правильность таких программ?

Об "алгоритмических ошибках" -- отдельно. Я так понимаю, что остальные ошибки -- синтаксические. У меня истерика была, когда я услышал, что "программа прошла синтаксическую отладку". Или Вы используете какую-то более подробную классификацию ошибок?

[bekas]

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

для уравнения Ax^2 + Bx + C = 0 возможные корни находятся
по формуле X1 = (-B + sqrt(B^2 - 4AC)) / 2 и X1 = (-B - sqrt(B^2 - 4AC)) / 2

Так вот, если взять A = 1, B = -100000, C = 1, то точные корни соответствующего
квадратного уравнения, правильно округленные до 11 значащих десятичных
цифр, суть X1 = 99999.999990, X2 = 0.000010000000001

Если мы воспользуемся школьными формулами, то вычислим
X1 = 100000.00 (очень хорошо)
X2 = 0 (совершенно неверно)

Имеются различные альтернативные способы вычисления корней квадратичного
полинома, которые избегают подобной потери точности, например:

X1 = -(B + sign(B) * sqrt(B^2 - 4AC)) / 2
X2 = C / (A * X1)

Такой способ дает X1 = 100000.00, X2 = 1/100000.00 = 0.000010000000;
оба результата вполне приемлемы.

Данный случай цитируется по книге "Машинные методы математических вычислений",
Дж. Форсайт, изд. "МИР", Москва 1980.

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

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

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

Или взять, к примеру, компилятор C++ Билли Гейтса. Сейчас мне приходится
выполнять разработку интерпретатора одного технологического языка
программирования. В целях оптимизации процесса интерпретации необходимо
было записать switch с довольно большим числом case. В результате среда
разработки IDE начинает валиться в самые непредсказуемые моменты. Думаю,
это связано с нехваткой памяти или переполнением буферов.

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

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

[незваный гость]

И что интересно, что правильность программы будет успешно доказана!

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

[bak]

ПОБЕДА РОССИЙСКИХ СТУДЕНТОВ

КАК и прогнозировалось на Чемпионате Мира-2006 по программированию вновь победа российских студентов
http://icpc.baylor.edu/icpc/Finals/default.htm

ЧЕМПИОНЫ МИРА-2006 - студенты САРАТОВСКОГО УНИВЕРСИТЕТА обошли и американцев и лучшие столичные вузы.

В десятке Лучших Команд Мира - 5 Российских ВУЗов. Это - общенациональная победа. И ЧИСЛОМ и УМЕНИЕМ. :roll:

Студенты Московского и Петербургского Университетов - в десятке лучших команд мира.

ТАК БУДЕТ еще 10-12 лет, пока в наших школах и вузах будут изучаться основы алгоритмизации с использованием языка РАЯ (Русского Алгоритмического Языка).

Алгоритмический Язык Ершова включал 3 правила структурирования алгоритмов: 1) последовательность (НАЧ-КОН), 2) альтернативы (ЕСЛИ-ТО-КОНЕЦ), 3) циклы (ПОКА-ЦИКЛ).

В СТРУКТУРНОМ ПРОГРАММИРОВАНИИ категорически запрещалось использование операторов go to ... (в русском переводе "пошел на ...")

ТЕОРЕМА Джакопини-Боома гласит, что для структурированных алгоритмов и программ существуют математические схемы анализа правильности по отношению к пред- и пост-условиям.

Харлан МИЛЗ на фирме ИБМ предложил в 1972г. документировать все программы с использованием структурного псевдокода.

В 1990г. фирма ИБМ объявила, что 15 лет не получала рекламацией на свою фирменную программную продукцию.

В 1985г. А.Ершов написал первый школьный учебник по информатике, в котором излагались основы алгоритмизации с использованием структурного алгоритмического языка (без ЭВМ).

С 2000г. российские студенты систематически побеждают и будут побеждать в чемпионатах мира по программированию: Петербург, Москва, Саратов, ...

[незваный гость]

bak писал(а):

ТАК БУДЕТ еще 10-12 лет, пока в наших школах и вузах будут изучаться основы алгоритмизации с использованием языка РАЯ (Русского Алгоритмического Языка).

Класс! Я охотно Вам верю. Это колоссальная, просто непреодолимая проблема американцев и индусов, что они не изучают РАЯ. Ну как же они, бедняги, корчатся, изучая англицкие ключевые слова в Java!

bak писал(а):

Алгоритмический Язык Ершова включал 3 правила структурирования алгоритмов: 1) последовательность (НАЧ-КОН), 2) альтернативы (ЕСЛИ-ТО-КОНЕЦ), 3) циклы (ПОКА-ЦИКЛ).

И Паскаль, в общем, тоже. Так что очередная Америка открыта. А какие классные русские слова -- НАЧ, КОН. Все понятно, все балдеют. Мне эти усилия Ершова и в 8ом классе были неприятны, и сейчас непонятны.

bak писал(а):

В СТРУКТУРНОМ ПРОГРАММИРОВАНИИ категорически запрещалось использование операторов go to ... (в русском переводе "пошел на ...")

У Вас какое-то примитивное представление о структурном программировании. Или это не определение (которое я просил)? Тогда что это?

bak писал(а):

ТЕОРЕМА Джакопини-Боома гласит, что для структурированных алгоритмов и программ существуют математические схемы анализа правильности по отношению к пред- и пост-условиям.

Ссылочку не дадите -- желательно на оригинал статьи? Я люблю такие статьи читать.

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

bak писал(а):

Харлан МИЛЗ на фирме ИБМ предложил в 1972г. документировать все программы с использованием структурного псевдокода. В 1990г. фирма ИБМ объявила, что 15 лет не получала рекламацией на свою фирменную программную продукцию.

Не буду утверждать наверняка, но, по-моему, в 1972 заметная часть програмной продукции IBM писалась на ассемблере. Для ассемблера документирование на псевдокоде -- большой шаг вперед.

То, что IBM "не получала рекламацией" внушает мне серьезно сомнение. Я не знаю ни одного пакета IBM без багов. И IBM очень внимательно работает со своими заказчиками по их локализации и путям обхода. Очевидно, кроме "фирменной" продукции (малая часть, только для ...), IBM выпускает нефирменные программы. Вот с последними-то мне и приходилось работать.

bak писал(а):

В 1985г. А.Ершов написал первый школьный учебник по информатике, в котором излагались основы алгоритмизации с использованием структурного алгоритмического языка (без ЭВМ).

А В.М. Глушков выступил с "безбумажной технологией" программирования. После чего количество потребляемой бумаги увеличилось... Сказать бы по-честному, что информатику изучать надо было, а купить хоть один PC на каждую школу не могли... Я уж не говорю про что-то лучшее, чем тогдашний PC.

[bak]

ПРОБЛЕМЫ АМЕРИКАНЦЕВ и ИНДУСОВ

ПРОБЛЕМЫ Американцев опубликованы в трактате СС-2001 - "Рекомендации по обучению информатике в университетах" http://www.apkit.ru/default.asp?artID=4980

НЕ УВЕРЕН, что Американцы хотят изучать информатику в своих университетах, также как и этого не хотят в МГУ.

В МГУ и в американских университетах в учебных планах нет курса информатики. Зато курс информатики есть почти во всех российских школах и вузах.

НАЗВАНИЕ ПЕРЕВОДА "Computing Curricula 2001" как "Рекомендации по обучению информатике в университетах" неправильное.

КНИГА очень хорошая. В ней изложены проблемы обучения программированию в американских университетах.

АСМ выработало общие рекомендации для американских университетов. Результат - с 2001г. русские систематически побеждают американцев

В редакции 2001г. описан опыт многих западных стран. Я внимательно изучал эту книгу еще в 80-ых годах.

В 2006 ГОДУ наконец-то MTI вошел в десятку лучших университетов, обогнав МГУ. Для американцев это достижение.

ВОПРОС: зачем это внедрять в российских вузах , если американские университеты проигрывают студентам из Саратова, Барнаула и Петербурга

Ну что тут поделать - американские учебники и учебные планы лучше А наши студенты переигрывают американцев

Наши профессора и преподаватели обучают лучше с намного худшей зарплатой в намного более худших условиях. ЭТО ФАКТ.

ОБРАТИТЕ ВНИМАНИЕ: Я не собираюсь скрывать свою фамилию, имя, отчество, звание и ученую степень. ВАК - это Виталий Адольфович Каймин.

ОБРАТИТЕ ВНИМАНИЕ2: На моих учебниках написано "Рекомендовано студентам вузов Министерством Образования РФ" по результатам победы в конкурсе.

В учебнике излагается техника и методика подготовки к экзаменам и олимпиадам по информатике для студентов и школьников.

Язык программирования при сдаче экзаменов может быть и Бейсик, и Паскаль, и С, и Фортран, и JavaScript.

Главное - получение на ЭВМ результатов решения прикладных задач, изучающихся в школах и вузах.

Правильность результатов определяется по постановке задач. Проверка решений на ЭВМ и на экзаменах, и на олимпиадах проводится с помощью тестов.

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

СТУДЕНТАМ и ШКОЛЬНИКАМ эта методика вполне доступна и понятна. Проверено неоднократно в различных вузах и школах Москвы и Российской Федерации.

ВАК, профессор, доктор Computer Science, автор российских учебников по информатике для студентов и школьников. http://bak2.narod.ru/inform.html

[Yuri Gendelman]

bak писал(а):

...Я не собираюсь скрывать свою фамилию, имя, отчество, звание и ученую степень...

Уточните пожалуйста, в какой стране Вы получили Вашу степень доктор Computer Science? Очень уж ПО-АМЕРИКАНСКИ она ЗВУЧИТ.

[незваный гость]

bak писал(а):

ВАК, профессор, доктор Computer Science, автор российских учебников по информатике для студентов и школьников. http://bak2.narod.ru/inform.html

Интересно. Я задал достаточно много вопросов, ни на один из которых Вы не ответили. Зато имя, которое нам известно с десяток дней, Вы написали, как откровение. Как если бы кто-то обвинил Вас, что Вы его скрываете.

1) Что же Вы хотите сказать участникам форума (за эти десять дней мы хорошо усвоили, что команда России побеждает на ACM ICPC, программа по информатике в России -- самая лучшая, а все это -- благодаря учебнику, Вами написанному)?

2) Понимаете ли Вы, что на данный момент Вы просто используете форум для саморекламы? Что дискурсия отсутствует? И что это может производить неприятное впечатление на остальных участников?

[Yuri Gendelman]

незванный гость писал(а):

bak писал(а):

ТЕОРЕМА Джакопини-Боома гласит, что...

Ссылочку не дадите -- желательно на оригинал статьи? Я люблю такие статьи читать.

C. Bohm and G. Jacopini. Flow diagrams, Turing machines and languages with only two formation rules. Communications of the ACM, 9(5), p.366-371, May 1966.
Доклад авторов на IFIP-1964 считается началом структурного программирования. Точная фамилия 1-го автора - B. Статья продается на сайте ACM (у меня ее нет). Думаю, сейчас она имеет только историческую ценность.
Кстати, скоро ее (статьи) 40-летие.

[незваный гость]

Спасибо за ссылку. А интересно? Если да, я попробую найти. А я то искал Giacopini.

[Yuri Gendelman]

незванный гость писал(а):

А интересно? Если да, я попробую найти. А я то искал Giacopini.

Я заинтересовался теор.программированием, когда наткнулся на книжки Ершова "Введение в теор. программирование" и Котова по теории схем программ. Но это было давно, с уклоном в параллельность и не на долго. А эта статья сейчас скорее для музея. Вроде Начал Эвклида. Но за предложение и good will спасибо.

[bak]

ЗАГЛЯНИТЕ В СОСЕДНИЙ РАЗДЕЛ

ЭТОТ РАЗДЕЛ - ноу-хау "НЕЗВАННОГО ГОСТЯ".

С ТЕЗИСОМ "Программы без ошибок - абсурд"
категорически не согласен. ЭТО - АБСУРД

Ощущение, что "НЕЗВАННЫЙ ГОСТЬ".
ни разу в жизни не отладил ни одной программы :?:

Загляните в книги Дийкстры - там все программы
приведены с доказательствами правильности.

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

Загляните в вузовские и школьные учебники информатики
- там много программ с доказательствами правильности.

Обучение на ошибках - это кошмар. Из этого кошмара
можно не выйти. Учебники с ошибками - это еще хуже.

Для разжигания дисскусий - это отличный прием.
Утверждение адсурда - это находка.

С анонимами дискуссий не веду. Ответов не даю.
Тем более, что Вы постоянно "передергиваете".

Приглашаю в раздел "Программы с ошибками - это КОШМАР"

[dikun]

bekas писал(а):

Или взять, к примеру, компилятор C++ Билли Гейтса. [...] В целях оптимизации процесса интерпретации необходимо было записать switch с довольно большим числом case. В результате среда разработки IDE начинает валиться в самые непредсказуемые моменты. Думаю, это связано с нехваткой памяти или переполнением буферов.

А можно взглянуть на ту часть кода, которая валит IDE (если, это, конечно, не комерческая тайна)? Какие именно глюки наблюдаются? Хотя бы примерно, какие действия пользователя IDE вызывают такие глюки? Что за версия IDE? Удалось ли Вам как-то справиться с ситуацией? Если да, то каким образом? Какие дополнительные примочки были установлены к IDE, кроме стандартных? На какой версии OS вертелась IDE?

[bekas]

Уважаемый dikun!

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

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

loop:

switch(*code++)
{

case aLDH_ZERO:
// реализация действия aLDH_ZERO
goto loop;
...
case aCALL:
// реализация действия aCALL
goto loop;
...
}

то становится очевидным самый главный тормоз интерпретатора - switch,
реализация которого на ассемблерном коде со всеми накладными расходами
может достигать 15 ассемблерных команд. Вот откуда, кстати, проистекает
показатель замедления 20 программы на JAVA (имеется в виду чистая интерпретация,
а не компиляция "на лету") по сравнению с C++. Я уж не говорю о том, что
switch каждый раз будет рвать конвеер команд.

Поэтому, чем больше действий вам удастся сосредоточить в одной микрокоманде
интерпретации, тем быстрее будет ваш интерпретатор. Например, многие системы
компиляции для выполнения действия *a++ = *b++ будут порождать несколько
ассемблерных команд (если иметь в виду что-то подобное RISC-архитектуре).

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

В результате обнаружилось, что самые последние версии VC6.0 (которые
объявляют о своей супер-оптимизации) в варианте Release не справляются
с трансляцией такого switch (им не хватает объема памяти даже в 2000МБ).

То же касается и системы компиляции для WINDOWS CE (в контроллерах у нас
применяется именно она). Приходится компилировать этот switch в режиме
DEBUG. А оболочка IDE "валится" в разные моменты (например, при переходе
к месту объявления переменной). Точно определить ситуации краха не удается,
но всегда идет ошибка по чтению памяти...

OS - WINDOWS XP, IDE без особых примочек

[bsivko]

незваный гость писал(а):

Серьезная программа -- это $10^4$ -- $10^7$ строк. Даже нижняя граница -- 170 страниц -- практически неприемлема для учебника. А для 10 строк другие законы.

Не соглашусь. Только не потому что отрицаю, а потому что считаю что ситуация другая и ваше видение имхо частично корректно.

Какова программа - большая или маленькая - от этого законы программирования не меняются.

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

незваный гость писал(а):

Если Вы посмотрите сообщения Debiloid'а в этой теме, то увидите, что он успешно автоматически доказывал правильность программ в 10-15 тысяч строк (пишу по памяти). Но обычно автоматические системы доказательства правильности основаны на непроцедурных языках.

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

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

незваный гость писал(а):

При этом возникает интересный вопрос -- написали Вы программу на псевдокоде, доказали ее правильность, а дальше что? Откуда следует правильность трансляции псевдокода в реальный язык? Откуда следует правильность формализации интерфейса используемых в программе пакетов или библиотек?

Да, именно так. Вы совершенно правы.
Но я скажу мнение с точки зрения той области, в которой работаю.
В общем случае для больших программных и аппаратно-программных комплексов нет ПО без ошибок. Но, для того, чтобы система работала стабильно, без сбоев, отказов и пр.. необходимо всеми возможными методами уменьшать вероятность ошибок.
С такой постановкой задачи мышление меняется. Нет понятия правильной программы, нет вопроса "а вдруг там ошибка?". Есть понятие программы, которая характеризуется неким уровнем ошибок. Этот уровень может выражаться как вероятностью нахождения ошибки, так (в зависимости от построения системы или комплекса) неким доказанным пределом (т.е. например что отказы могут проявляться не чаще чем 1 раза в год по вине системы). И для достижения такой цели имеется под рукой ряд средств, позволяющих повысить качество ПО.

незваный гость писал(а):

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

Hint: Авиация и медицина не самые требовательные области по качеству ПО.

Как раз таки в системах, где предъявляются серьезные требования по надежности и безопасности функционирования, и проявляется ниша, в которой нужно доказательство правильности. Да, никто не проводит доказательство для всего ПО системы. Доказательство проводится для малых модулей, которые критичны к безопасности. Сама же система строится с использованием ряда методов и средств, позволяющих снизить проявление ошибок любого рода. Здесь доказательство - метод поиска ошибок, а также метод построения безопасных и надежных малых модулей.

незваный гость писал(а):

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

Никакое дублирование или резервирование не спасает от алгоритмических ошибок. (см. например катастрофу Ariane)

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