2026年7月4日 分散プロトコルは単体テストできないが、モデル検証はできる 分散バグはデプロイ後の修正コストが高い。モデル検証を使えば、実装コードを1行も書く前にそれらを発見できる。以下はTLA+を使った方法である。 model-checkingdistributed-systemstlaplusprotocol-design
2026年6月1日 Webサービスにグレースフルシャットダウンがある。それがバグだ。 クラッシュオンリーソフトウェアは、あらゆる障害をクラッシュとして扱い、あらゆる起動をリカバリーとして扱う。Webサービスにとってこれは、シャットダウンロジックを削除し、kill -9でも生き残る状態を設計することを意味する。 deep-divescrash-only-softwareresiliencedistributed-systems
