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

Насколько я понимаю в пайтоне единственная стратегия управления памятью -- сборка мусора.

>> Раст позволяет кодировать эти соглашения в API. И проверяет
>> чтобы API соответствовало коду. Причём он проверяет, чтобы реализация API соответствовала
>> бы заявленному в API. И он проверяет, чтобы код, пользующийся API,
>> пользовался бы им так, как требует выбранная стратегия управления памятью.
> Эта задача там действительно решается или "мамой клянус, в 99% случаев это
> сработает"?

"мамой клянус". Есть ведь unsafe который позволяет тебе творить всё, что возможно творить в C. Есть unsafe inline asm, который позволяет тебе творить всё, что позволяет asm.

> Проверка корректности программ в общем случае - задача алгоритмически
> не менее безнадежная чем сравнение двух вещественных чисел.

Во-первых, здесь не об общем случае доказательства корректности. Речь о безопасности работы с памятью.

Во-вторых, ... лирическое отступление. Опеннет влюблён в миф о том, что достаточно квалифицированный программист на C может писать безбажные программы. Если мы допустим, что этот миф верен, то из него вытекает, что этот программист про свои программы может доказать их корректность. У него есть в голове какой-то способ это доказать, этот способ -- часть его квалификации. Если он не может доказать, то каким образом он знает, что вот теперь его программа корректна? Вся теория идёт лесом: если теоретически невозможно доказать в общем случае, значит этот программист практически выбирает такие _частные_ случаи (такие способы написать программу), в которых доказательство корректности возможно.

Доказать корректность про целую программу на C практически невозможно. Если это невозможно только потому, что внимания и терпения недостаточно, то это ситуация, с которой C'шные программисты вынуждены мириться, и поэтому она считается нормальной. Но если C'шный программист не видит способа как можно было бы доказать, имея достаточно внимания и терпения, то ему надо переписывать свою программу или быдлокодер. То есть, если у меня в программе есть массив, если я подозреваю, что индекс может выходить за границу его... если я подозреваю, но не знаю, это значит, что я не могу доказать корректность своей программы, это значит, что это гумно, а не программа. В большинстве случаев, когда упираешься в такое, всё же доказываешь -- либо находишь баг и исправляешь его, либо доказываешь корректность. Но мне приходилось переписывать шматы кода, потому что я не понимал, почему они работают: программа падает, почему падает непонятно, падает явно не в том месте кода, где ошибка. Но в программе есть какой-то кусок кода, который я не понимаю -- может из него иногда вылетает висящий указатель? Хз. Доказать не могу, опровергнуть тоже. Начхать, нахрен такой код, я вот сейчас напишу такой, который я буду понимать и про который докажу, что из него не вылетает висящих указателей.

Так вот, _во-вторых_, раст позволяет тебе инкапсулировать unsafety в модулях, чтобы оно если и протекало через границы модулей, то явно и контролируемо. Если ты про каждый модуль с блоками unsafe доказал его safety, разглядывая его в отдельности, если ты затем отдельно разобрал каждый вызов unsafe функции пересекающий границы модулей, и если в процессе выстраивания доказательств ты не совершил ошибок, то ты выстроил доказательство safety. Фишка в том, что тебе не придётся выстраивать доказательств, которые ссылаются на много разных файлов с кодом. Каждое доказательство в отдельности будет ссылаться только на код одного файла. Исключения могут возникать только когда ты вызываешь unsafe функцию из другого модуля.

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