Здравствуйте, MaxxK, Вы писали:

MK>>>... что, в свою очередь, ничуть не мешает программам в плохих случаях (1) уйти в бесконечный цикл или (2) съесть всю доступную память, так и не решив при этом задачу. От (1) Coq защищает по построению, а вот для (2) я, к сожалению, не слышал о каких-то красивых общих подходах.

I>>И что с того ?

MK>Но при этом понять, какого количества памяти будет достаточно, в общем случае для программ, написанных в Coq, нельзя.

Ну вот ты сам себе дал объяснение. Потому утверждать "полнота по Тьюрингу не нужна" мягко говоря преждевременно. Пока что никто не продемонстрировал внятный инструмент, который решит насущные задачи нежели языки с полнотой по Тьюрингу. вот и всё.