Ответ 1
Многие программисты приравнивают статическую проверку типов к безопасности типов:
- "язык A имеет статическую проверку типов и поэтому безопасен для типов"
- "язык B имеет динамическую проверку типов и поэтому не является безопасным для типов"
К сожалению, это не так просто.
В реальном мире
Например, C и C++ не являются типобезопасными, потому что вы можете подорвать систему типов с помощью Type punning. Кроме того, спецификации языка C/C++ в значительной степени допускают неопределенное поведение (UB) вместо явной обработки ошибок, и это стало источником эксплойтов безопасности, таких как эксплойт с разрушением стека и атака форматной строки. Такие эксплойты не должны быть возможны на типобезопасных языках. В ранних версиях Java была ошибка типа с ее Generics, которая доказала, что она не полностью безопасна для типов.
До сих пор для языков программирования, таких как Python, Java, C++,... трудно показать, что эти языки полностью безопасны по типу, потому что они требуют математического доказательства. Эти языки массовые, и у компиляторов/интерпретаторов есть ошибки, о которых постоянно сообщают и исправляют.
[ Википедия ] Многие языки, с другой стороны, слишком велики для созданных человеком доказательств безопасности типов, так как они часто требуют проверки тысяч случаев.... некоторые ошибки могут возникать во время выполнения из-за ошибок в реализации или в связанных библиотеках, написанных на других языках; такие ошибки могут сделать данный тип реализации небезопасным в определенных обстоятельствах.
В академии
Безопасность типов и системы типов, хотя и применимы к реальному программированию, имеют свои корни и определения, исходящие из научных кругов, и поэтому формальное определение того, что именно является "безопасностью типов", встречается с трудностями, особенно когда речь идет о реальных языках программирования, используемых в реальных Мир. Академикам нравится математически (формально) определять крошечные языки программирования, называемые игрушечными языками. Только для этих языков можно формально показать, что они безопасны по типу (и доказать, что операции логически корректны).
[ Википедия ] Безопасность типов обычно является обязательным требованием для любого игрушечного языка, предлагаемого в академическом исследовании языка программирования.
Например, ученые изо всех сил пытались доказать, что Java безопасна для типов, поэтому они создали уменьшенную версию под названием Featherweight Java и доказали в статье, что она безопасна для типов. Точно так же этот доктор философии статья Кристофера Лиона Андерсона взяла подмножество Javascript, назвал его JS0 и доказал, что он безопасен для типов.
Практически предполагалось, что надлежащие языки, такие как python, java, C++, не полностью безопасны по типу, потому что они очень большие. Крошечному жучку так легко проскользнуть сквозь трещины, которые могут подорвать систему типов.
Резюме
- Ни один python, вероятно, не является полностью безопасным для типов - никто не доказал это, это слишком сложно доказать. Скорее всего, вы обнаружите небольшую ошибку в языке, которая продемонстрирует, что она не является типобезопасной.
- На самом деле, большинство языков программирования, вероятно, не полностью безопасны по типу - все по тем же причинам (доказано, что только игрушечные академические)
- Вы действительно не должны верить, что языки со статической типизацией обязательно являются безопасными типами. Они, как правило, безопаснее, чем языки с динамической типизацией, но говорить, что они полностью безопасны по типу с уверенностью, неверно, поскольку нет никаких доказательств этого.
Ссылки: http://www.pl-enthusiast.net/2014/08/05/type-safety/ и https://en.wikipedia.org/wiki/Type_system