型安全性２

単純に「クラッシュしない」ことだけではなく、「許可ないし定義されていない操作は実行されない」ことが重要なのです。抽象型とか線形型とか情報流型とか、と我田引水。

もし本当にすべて型理論で保証したかったら、Coqとかの依存型で証明（＝プログラム）と定理（＝型）を一緒に記述する、というのがもっともラディカルなアプローチかと。正しさが証明されたCコンパイラやファイル同期ソフトぐらいは書けるようですし。

研究から普及まで何十年もかかるのはまた別問題。多相型や型推論もそうでしたし、型じゃないけど、たとえばガベコレもLispからJavaまでかかったわけで。