Статья 431

Хотя не совсем понятно, как можно называть эффективной неправильную программу. Но представим себе, что имеющиеся в программе ошибки так редки, что могут оставаться незамеченными годами, не приводя при своем появлении к трудно устраняемым последствиям. В подобных условиях неправильная в строгом смысле, но эффективная программа может оказаться более предпочтительной, чем неэффективная правильная. Напротив, если речь идет о доказательстве математической теоремы с использованием компьютера или если ошибка в программе способна повлечь за собой необратимые последствия, катастрофу, например, тщательное доказательство правильности становится просто необходимым, о чем мы еще поговорим ниже.
Разумеется, лучше всего, если правильность и эффективность мирно уживаются в одной и той же программе. С этой точки зрения разобранные выше программы далеки от идеала. Но цель рассмотренных здесь простых примеров состояла лишь в демонстрации некоторых ключевых идей, связанных с доказательствами правильности программ.