構造的正しさ
ソフトウェアの正しさを「構造的正しさ」という観点から考察する記事。単なる機能的正しさ（expected behavior）を超え、コードやシステムのアーキテクチャが本質的に健全であることの重要性を論じる。構造的正しさは、時間が経ってもシステムが堅牢で保守しやすい状態を維持するための基盤となる。
背景メモ
- データベースや分散システムの文脈で「正しさ」を議論する際に伝統的に使われてきたのは「線形化可能性」（linearizability）や「逐次一貫性」（sequential consistency）といった一貫性モデルだが、これらは歴史的に「操作」を単位として定義されている。
- 著者のSao（@sao_nyc）はデータベース内部構造の研究者・実装者で、特に分散トランザクションや検証技術を扱う。ブログ記事は技術的に深い内容が多い。
- 本記事は、既存の「操作ベース」の正しさの定義では捉えきれないバグ（例：ページフォーマットの破損や領域外書き込み）が存在することを指摘。その対策として「構造的正しさ」（structural correctness）という概念を提案し、不変条件（invariant）やメモリ安全性の観点からシステムを検証する枠組みを論じている。
- 背景として、近年「TLA+」や「形式検証」への関心が高まっているが、それらは主に操作の仕様（spec）レベルでの正しさを保証する。構造的正しさはそれより低レイヤー（実装レベル）の安全性を扱う。