グローバルプロパティのためのローカル推論
本稿では、分散システムや並行プログラミングにおいて、グローバルな特性（データ整合性や一貫性など）を保証するために、ローカルな推論手法をどのように活用できるかを考察する。従来のグローバルな解析はスケーラビリティに欠けるが、ローカルな観察と推論を組み合わせることで、効率的かつ堅牢な検証が可能になることを示す。
背景メモ
- Laurie Tratt氏（英ボーンマス大教授）による、ソフトウェアの「局所的推論」と「大域的性質」のギャップを論じた記事。
- 「局所的推論」とは、関数やクラスなどコードの一部分だけを見てその振る舞いを理解できること。「大域的性質」とは、システム全体で成り立つべき性質（例：メモリリークがない、デッドロックしない）。
- 静的型付けや所有権システム（Rustの所有権モデルなど）は、このギャップを埋めるために設計されているが、完全には解決できないと論じる。
- 具体的な例として、参照カウントの循環参照や、楽観的ロックのバグを挙げ、どんなに優れた型システムでも本質的に捉えきれない大域的性質が存在することを示す。
- 記事の結論としては、完璧な解決策はなく、設計原則の選択（関数型 vs オブジェクト指向、静的 vs 動的型付け）すら本質的には優劣がつけがたいと述べる。