«Проверяет другую программу» очень широк. Фактически, некоторые функции программ можно проверить , например, проверяет ли тип программы Java. Тем не менее, проверка типов в Java-программе также отвергнет некоторые программы, которые никогда не приведут к ошибке типа при запуске, например:
int foo() {
if (true) return 5;
else return null;
}
Этот метод никогда не вернет null, но средство проверки типов не может этого увидеть. Но разве мы не могли бы сделать систему более умного типа?
К сожалению, ответ - нет. Рассмотрим следующую программу:
int bar() {
if (infiniteComputation()) return 5;
else return null;
}
Средство проверки типов не может проверить, будет ли infiniteComputation когда-либо возвращать false, из-за проблемы остановки .
Другая связанная теорема - Теорема Райса , которая, вероятно, ближе к тому, о чем был задан ваш вопрос, чем к проблеме остановки.
Стоит отметить, что в теореме утверждается только то, что нет программного свойства, которое можно было бы точно проверить, но все еще можно достаточно хорошо аппроксимировать такие проверки для практических целей. Одним из примеров являются системы типов, где мы принимаем, что некоторые «правильные» программы отклоняются, как фрагмент кода выше. Компиляторы также могут устранять мертвый код во многих случаях, хотя это невозможно сделать в в каждом случае.