Комментарии 12
Вот вы здесь формально доказали логически обосновали какой-то свой тезис. Но ведь и правда - на практике все может быть по-другому. Выходит, что зря потратили время, лучше бы делом занялись) Ну и что что пятница.
99% проблем из-за того, что абсолютно корректно написанная программа на абсолютно безопасном языке совершенно верно исполняет неправильное ТЗ. Они же — «неверная модель объекта управления» (для промышленного ПО это называется так, но во всех сферах есть аналоги).
"Без внятного ТЗ - результат ХЗ" :-)
Мне всегда казалось что доказательное программирование - это не про этап выполнения а про результат компиляции. Что мы можем доказать, что на процессоре, как машине тьюринга, скомпилированный код приведёт к корректному ответу на корректных входных данных.
А это все уже доказывается на уровне математики - программа превращается в конечный автомат и доказывается соотвествие входных состояний выходным. (Ну это как я себе это вижу, скорее всего эксперты опишут это намного адекватнее)
А ошибки на уровне физики процессора или уж крайне маловероятное попадание космических лучей - это не про программирование вообще, а про риск менеджмент - в конце концов на ваш компьютер кирпич может упасть, но причём тут программирование?
но причём тут программирование?
Так программирование нужно не само по себе. Нужен корректный результат выполнения программы. Естественно, что если программа написана неправильно, то и результат её выполнения будет неправильным.
Однако обратное утверждение неверно (что у правильной программы будет корректный результат выполнения), т.е. корректность самой программы (отсутствие в ней ошибок), это обязательное, но не достаточное условие получение правильного результата её выполнения.
Сколько раз за свою жизнь вы лично видели корректно написанную программу? Я даже не спрашиваю про ее запуск и ничего не спрашиваю про железо на котором она запускалась.
Вы сначало решите вопрос с корректностью программы хотя бы с сосписком оговорок типа ансэйф код не учитываем, ось не учитываем и т.д.
Короче говоря зачем вы нам рассказываете о том что там у них негров линчуют когда у вас спрашивают конкретно про вашу ответственность в вашей зоне ответственности - корректность вашего кода. Вот когда вы докажите, что он у вас корректен вот тогда у вас и появиться право переводить стрелки на других, а пока это не произошло то ...
В общем за свою жизнь я ещё не разу не видел и даже не слышал про существование хотя бы одной корректной программы даже с большим списком оговорок.
Суть статьи в одном обзаце. Процессор или память могут сбоить - факт. Поэтому, ну его нахер писать корректные программы - оч странная логика, на мой вкус.
Тут надо определиться мы про доказательное программирование говорим или про рациональность его применения.
Для меня статья выглядит как осуждение автомобиля, за то что в городе нет дорог.
Если в твоём городе нет дорог - очевидно что автомобиль тебе не подходит, но это не "миф об автомобиле" - как в заголовке статьи)
Если для конкретной задачи ошибка из за попадания космических лучей или сбоя физики процессора критична, это не значит что доказательное программирование плохо или не работает)
Если математически доказанная корректность программы не гарантирует защиту от непредвиденных аппаратных сбоев, то следует ли вкладывать ресурсы в формальные методы доказательной безопасности языка или же сосредоточиться на механизмах резервирования и устойчивости, и как найти оптимальный баланс между этими подходами?
Формальные методы доказательства безусловно нужны. Иначе если на входе ерунда, то на выходе тоже будет ерунда при любой аппаратной платформе и проблема действительно именно в балансе.
И если речь заходит о любых ресурсах, то самый лучший способ нахождения баланса, это анализ экономики. т.е. сравнение тех или иных решений с финансовой точки зрения (и возможно с учетом статистики). Это чисто менеджерская задача из области управления проектами, которая вообще не имеет к написанию программного кода никакого отношения.
Миф о доказательном программировании без ошибок