types - 強い型付けは型の安全性を意味しますか？

Question

コンパイラコースの講義ノートを確認していますが、スライドの1つに次のように書かれています。

強く型付けされた言語は、受け入れられたプログラムが型に対して安全であることを保証します

しかし、私はこれの証拠を他の場所で見つけることができません。

たとえば、ウィキペディアでは、強い型付けを行う言語としてc ++がリストされていますが、型安全性が低い言語としてcもリストされています。

それで、取引は何ですか？スライドが間違っているのでしょうか、それとも何か見落としているのでしょうか。

ウィキペディアの強い型付けの例

Answer 1

「強く型付けされた」は、あまり明確に定義された概念ではありません。これはおそらく、より正確なメモリセーフの同義語として最もよく解釈されます（つまり、プログラムが未定義の動作によって自身のメモリを破壊することは決してありません）。

型理論では、「強く型付けられた」という用語は使用されません。代わりに、サウンドタイプのシステムについて話します。さらに、適切でないタイピング規則のセットは、通常、適切な型システムとはまったく見なされません。

非公式な使用法では、「強く型付けられた」は「動的に型付けされた」言語にも適用されます。これは、理論的な観点からは、さらに意味がありません。型理論の用語では、これらの言語は型付けさえされていません。

ずっと前に、Luca Cardelliは、型付き/型なしと安全/安全でないという2つの独立した次元を区別することにより、言語の安全性のより一貫性のある分類を導入しました。アセンブリは型指定されておらず安全ではありません。Cは型付けされていますが安全ではありません。JavaScriptは型付けされていませんが安全です。JavaまたはMLは型付けされて安全です。たとえば、http ：//www.lucacardelli.name/Papers/TypeSystems.pdfを参照してください。