システム設計の2つの抽象化：隠すか、削るか

The Two Abstractions of System Design: Hide or Reduce

分散システム研究者がTLA+などのモデリングで重要視する「抽象化」は、CS教育で教わる従来の抽象化とは根本的に異なる。モジュール化抽象化は内部を隠して境界を引くのに対し、モデリング抽象化は対象の性質に本質的な部分だけを残してシステムを切り詰める。この違いを理解することで、モデリングのスキルギャップの謎が解ける。Lamportの論理クロックやPaxos、線形化可能性など、分散システムの設計はモデリング抽象化の好例だ。