1. Introduction

1.1 Types in Computer Systems

型システムはプログラムの正しさを与えるための formal method である。つまりある一定の間違えようのない方法に従って、プログラムの正しさが保証できる。
- 他にもそういう方法ってのはあるらしい。
- より正確には一部の正しくないプログラムの正しくなさを、プログラムを実行せずに検出できる。
動的型付け言語は「dynamically checked language」と呼んだほうがよさそうらしい。
- 上の話からすれば、動的型付けで得られるのはプログラムの正しさというよりは実行時の安全性（メモリを意図せず破壊しないとか）にすぎないということだろう。

…in principle each type system comes with a definition of the behaviors it aims to prevent. The safety (or soundness) of each type system must be judged with respect to its own set of run-time errors.

— p.3

型安全ってのはその言語がどういう実行時エラーを防ぎたいか、ということとあわせて考えられるべきもの。