OberonCore

Вот видите как здорово! С рекурсиями ваши циклические инварианты нафик не нужны...

В смысле -- правильная рекурсия сама себе инвариант!

Если частный случай рекурсии - это цикл, тогда логично предположить, что частный случай её инварианта - инвариант цикла.

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

Приходим практически к Эйфелю Бертрана Мейера.
Книжка 1500 страниц

А там разве инварианты статически проверятся, при компиляции? Не помню, что бы писалось об этом -- вроде только динамически...

Седни посмотрю дома в книжку - мож чего написано подробнее.
Статически инвариант же не проверить.
Статически - это доказательство правильности.

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

Гениально. Может, вообще всё будем статически вычислять?

Все что можно - да.

Те инварианты, которые можно проверить статически, тривиальны.

Разница между статикой и динамикой - это разница между полной разрешимостью и частичной (знаём всё множество интересующих нас вещей; или всего лишь имеем возможность относительно каждого конкретного объектов - конкретного хода выполнения - проверить его принадлежность к множеству).

Разница фундаментальная, и хоть убей себя ап стену Ну дык программёрам закон не писан.

Сначала получите её - правильную.
Проведите доказательство рекурсии - через неподвижную точку функции и т.п. - повеселитесь.

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

Да нет. Это определение тривиальности вообще.

Ну почему же не писан.
Просто о разных вещах говорится. Влад, как я понял, намекает на то, что нужно максимально применять что-то вроде шаблонов - для вычислений на этапе компиляции.
Смотрим на Ершова и его смешанные вычисления. Статика - это как раз подстановка максимально возможного количества известных параметров. А все, что осталось - это и есть исполняемая программа.
Ну, и ИМХО, "всего лишь имеем возможность проверить... принадлежность множеству" - это и есть РЕАЛЬНЫЕ задачи. Ибо множества, как правило либо бесконечные, либо очень большие...