THEマルチプログラミングシステム
ユーザー層(ダイクストラは「我々は実装していない」と述べている)
上位層が下位層にのみ依存するという制約を課したのは、(準形式手法的に)システムの挙動を推測しやすくし、システムを段階的に構築できるようにするためである。システムは Layer 0 から順に実装され、それぞれの層が提供する抽象化を順に試験していった。この形式手法的設計プロセスは大いに成功し、ダイクストラは次のように述べている。
我々は、論理的健全性が演繹的に証明できる方法で洗練されたマルチプログラミングシステムを設計可能であり、その実装が徹底的な評価に耐えることを見出した。評価中に見られた誤りは瑣末なコーディング上の誤りだけであり(500命令に1回の割合で発生した)、10分程度のマシンでの調査で個々の問題を検出でき、その対処も容易であった。
このようにカーネルを階層化するという方式はMulticsのリングプロテクションモデルに似ている。その後のOSは何らかの階層化を導入していることが多く、例えば Windows NT や macOS がそうだが、階層の数はTHEシステムより少ない。
動作プラットフォームはオランダの Electrologica X8 コンピュータで、システム自体はアセンブリ言語で書かれている。このコンピュータは32キロワードの磁気コアメモリ(1ワードは27ビット)、LRU方式のバッキングストアを備えた512Kワードの磁気ドラムメモリ、紙テープリーダー・パンチャー、プリンターを備えていた。