История изменений

Тогда можно использовать заведомо недостижимое число шагов и проверять бесконечные программы? То есть проверка будет «либо значение нужного типа, либо в ближайшие 20 миллиардов лет программа не завершится».

Да. Именно Кок интересуется лишь теоретической завершаемостью. Т.е. он должен доказать что программа [а точнее запускаемая в коке функция] завершиться в принципе. Время завершения его по умолчанию не интересует.

Но если ты такое условие ставишь, ты сам понимаешь что твой код надёжным не является.

На практике для программирования это не применяется на сколько я знаю. Думаю, хотя бы потому что монады при экспорте кода [в окэмль, для скорости] дадут большой оверхэд при выполнении (хотя может можно как то придумать, не знаю).

Это удобно например для трансляции императивных программ [в coq с целью доказательства их корректности]. Императивные программы транслируют в монады (руками или автоматически). Тут важно чтобы всё скомпилировалось, поэтому монады очень удобны. И не важно какое число передавать в run поскольку код запускать никто не будет. А потом доказывают что всё-таки всё завершится когда надо и без ошибок. Ну или не доказывают. Или ошибки находят, потом поправляют, а потом всё таки доказывают...

Тогда можно использовать заведомо недостижимое число шагов и проверять бесконечные программы? То есть проверка будет «либо значение нужного типа, либо в ближайшие 20 миллиардов лет программа не завершится».

Да. Именно Кок интересуется лишь теоретической завершаемостью. Т.е. он должен доказать что программа завершиться в принципе. Время завершения его по умолчанию не интересует.

Но если ты такое условие ставишь, ты сам понимаешь что твой код надёжным не является.

На практике для программирования это не применяется на сколько я знаю. Думаю, хотя бы потому что монады при экспорте кода [в окэмль, для скорости] дадут большой оверхэд при выполнении (хотя может можно как то придумать, не знаю).

Это удобно например для трансляции императивных программ [в coq с целью доказательства их корректности]. Императивные программы транслируют в монады (руками или автоматически). Тут важно чтобы всё скомпилировалось, поэтому монады очень удобны. И не важно какое число передавать в run поскольку код запускать никто не будет. А потом доказывают что всё-таки всё завершится когда надо и без ошибок. Ну или не доказывают. Или ошибки находят, потом поправляют, а потом всё таки доказывают...