- RustとGoのバックグラウンドを持つ筆者は、型システムが足を撃つことを防いでくれるので好んでいる。
- Richard EisenbergがJane StreetのThe Future of Programmingで話した内容により、プログラミング言語、型システム、コードの未来について考えさせられた。
- Eisenbergは依存型について語り、型が値に依存できるという概念について述べた。
- Rustの所有権モデルがメモリセーフティにおけるシートベルトであるなら、依存型は何も間違えないようにNASAの制御室全体と言える。
- 例えば、配列が常にソートされていることを型レベルで保証したい場合、RustやGoではテストを書くが、Haskell（依存型を使用）ではこれを型システムにエンコードする。
思ったこと:
プログラミング言語の進化において、依存型が重要な役割を果たす可能性がある。安全性や正確性を保証するために、型システムがより柔軟で表現力豊かになることは、開発者にとって大きな利点となるだろう。