Исправление xaizek, (текущая версия) :
Любой возможный побочный эффект практически сразу же перечёркивает всё доказательство корректности в рамках конкретной единицы проверки. В ФП побочных эффектов по умолчанию нет, поэтому там проще. Аналогичный нативный язык должен быть сильно ограничен в операциях, чтобы формальное доказательство было возможно.
Не удивлюсь, если какой-нибудь подобный академический язык есть.
Исходная версия xaizek, :
Любой возможный побочный эффект сразу же перечёркивает всё доказательство корректности в рамках конкретной единицы проверки. В ФП побочных эффектов по умолчанию нет, поэтому там проще. Аналогичный нативный язык должен быть сильно ограничен в операциях, чтобы формальное доказательство было возможно.
Не удивлюсь, если какой-нибудь подобный академический язык есть.