Исходное сообщение
"Выпуск языка программирования Rust 1.48" Отправлено red75prime, 20-Ноя-20 11:21
Неразрешимость проблемы остановки означает, что существует программы, для которых невозможно доказать остановятся они или нет. Для всех остальных программ это доказать можно. То есть написать доказанно останавливающуюся (или не останавливающуюся) программу можно и на Тьюринг-полном языке. Но для этого сначала нужно написать конструктивное доказательство существования решения проблемы, и по этому доказательству построить программу. Такая программа существует согласно cоответствию Карри — Ховарда. Да, существуют Тьюринг-неполные языки, в которых любая компилирующаяся программа останавливается, но для написания доказанно-останавливающихся программ они не обязательны. Проблема возникает только если мы пишем программу, а потом пытаемся доказать, что она останавливается. В общем случае это невозможно. Но всегда можно эту программу подкорректировать так, чтобы она решала нужную задачу и доказуемо останавливалась. Если этого сделать нельзя, значит не существует такого доказательства для нашей задачи. То есть задача просто неразрешима и написать программу для её решения невозможно. В этом случае переформулируют задачу. TL;DR Проблема остановки особого практического значения не имеет.