Является ли сильная печать подразумеваемой безопасностью типа?

Question

Я обзор лекций для курса составителей, и один из слайдов говорит:

строго типизированных языков гарантирует, что принятые программы типобезопасный

Однако, я не могу найти любые доказательства этого в другом месте.

Например, wikipedia перечисляет C++ как язык с сильной типизацией, но также перечисляет c как язык, который не является безопасным по типу.

Итак, в чем заключена сделка? Являются ли слайды неправильными или я что-то пропустил?

Wikipedia's example of strong typing

Answer 1

«Сильно типизированный» не очень хорошо определено понятие. Вероятно, это лучше всего интерпретировать как синоним более точного памяти-безопасности (т. Е. Программа никогда не сможет испортить собственную память через неопределенное поведение).

В теории типов терминология «строго типизирована» никогда не используется. Вместо этого говорят о звуковых системах. Более того, любой набор правил ввода, который не является звуковым, обычно не рассматривается как правильная система типов.

В неформальном использовании термин «строго типизированный» также применяется к «динамически типизированным» языкам, что с теоретической точки зрения имеет еще меньший смысл. В терминологии теории типов эти языки даже не типизированы.

Давным-давно Luca Cardelli ввел более согласованную классификацию языковой безопасности, выделив два независимых измерения: типизированные/нетипизированные и безопасные/небезопасные. Сборка является нетипизированной и небезопасной, C напечатан, но небезопасен, JavaScript является нетипизированным, но безопасным, а Java или ML набраны и безопасны. См. http://www.lucacardelli.name/Papers/TypeSystems.pdf