> В общем случае доказать "корректность" произвольной программы, написанной на тьюринг-полном языке  невозможно. Это доказал Тьюринг в 1936 г.
> см. "Проблема остановки"
> https://en.wikipedia.org/wiki/Halting_problem

1) В общем случае это верно для машины Тьюринга с _бесконечной_ лентой. Только вот у нас в реальности память - конечная, как бы современные вебпогроммисты не пытались уверить в обратном.
> any finite-state machine, if left completely to itself, will fall eventually into a perfectly periodic repetitive pattern. The duration of this repeating pattern cannot exceed the number of internal states of the machine... (Minsky 1967, p. 24)

Ну и да, все возможные варианты программ никому, кроме теоретиков, никуда не упали. На практике интересно подмножество, решающее какие-то реальные задачи.

2)
> Rust можно считать тьюринг-полным языком, поэтому автоматическое доказательство "корректности" любой программы написанной на Rust невозможно.

"нельзя доказать в общем случае => значит нелзя доказать для частного случая"
Л-логика.