Означает ли строгая типизация безопасность типов?

Question

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

Строго типизированные языки гарантируют, что принятые программы безопасны для типов

Тем не менее, я не могу найти никаких доказательств этого в другом месте.

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

Так в чем же дело? Слайды неправильные или я что-то пропустил?

Пример строгой типизации в Википедии

Answer 1

"Сильно типизированный" не очень четкое понятие. Это, вероятно, лучше всего интерпретировать как синоним более точного безопасного для памяти (то есть, программа никогда не может повредить свою собственную память из-за неопределенного поведения).

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

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

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