Статья 351

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