> -- Peter Almazov писал(а):
> не ведет к построению правильного цикла.

Какая разница, каким способом построить правильный цикл?
Идея Info21 относительно ЦД в том, что ЦД позволяет многие циклы вывести из категории "требует полностью формального вывода" в категорию "очевидно и правильно строится путём анализа семантики задачи".
Второй вариант более желателен, тогда как первый нужно применять только, если невозможен второй (с этим обычно не соглашаются математики и спорят с физиками и инженерами).

Напоминаю, что доказать - это не значит провести какие-то "священнодействия", а это значит предоставить проверяемую вещь в такой форме, в которой в её правильности может убедиться любой желающий.

Для инженерной практики введение более простых способов обеспечить надёжность - это прогресс... Иначе "полным методом" так и будут пользоваться единицы.