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

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

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

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

Почему преждевременно? Для программ «обычного человека» у нас есть характеристики корректности «наверное не упадёт», «наверное посчитает правильный ответ», «наверное не повиснет» и «наверное хватит памяти/стека». Для программ «курильщика Coq» эти характеристики — «точно не упадёт», «точно посчитает правильный ответ», «точно не повиснет», «наверное хватит памяти/стека». 3 гарантии из 4 (да даже 1 из 2, как в исходном примере), на мой взгляд, вполне себе повод для заявлений «полнота по Тьюрингу не нужна».

Если же порассуждать о том, как мог бы выглядеть внятный инструмент для доказательства характеристик по памяти, то неполные по Тьюрингу предметно-ориентированные языки с линейными (как в Rust) типами, или какая-то система и с линейными, и с зависимыми типами, мне кажутся многообещающими направлениями. Неполнота по Тьюрингу здесь появляется не сама по себе, а как необходимое условие корректной работы анализаторов кода.

Но пока у нас в production, к сожалению, не наступило светлое будущее даже с позиций избавления от стандартных ошибок при работе с памятью, не говоря уже о доказательствах корректности реализации алгоритмов. Поэтому (насколько видно мне, могу ошибаться) гораздо больше работ по извлечению пользы из Тьюринг-неполных языков публикуется именно по этим направлениям.