TLA+が検証できないもの、それは何か
What TLA+ can and can't check
Claude Codeの開発者がOpusによるTLA+での競合状態発見を報告し、形式検証への期待が高まっている。TLA+の長年の教育者である著者は、その熱狂に警鐘を鳴らす。TLA+は不変条件や活性といった安全性・活性プロパティの検証に優れるが、到達可能性やハイパープロパティなど、表現すらできない性質も多い。仕様がコードの正しさを保証しない点と合わせ、過度な期待を戒める。
もし鳥という人間の概念を形式化できなければ、あなたのアプリが鳥を認識することを証明することはできない。
HNでの議論
30- sourdecor
HNのこのコメント[1]のおかげでQuint[0]を知った。Quintは「実行可能な仕様記述言語（JavaScriptで動作する）で、TLA（temporal logic of actions）に基づく素晴らしいツール群を備えている」。これは最高だと思うし、TLA+に興味がある人は誰でもチェックすべきだ。
- singron
これは素晴らしい。TLA+を何かに使おうとしている人にとっては読む価値のある記事だ。
別の観点では、TLA+が苦手とするもう一つのものはアトミック操作のモデリング、特に弱いメモリセマンティクスや逐次一貫性以外のものだ。アルゴリズムをpcalに変換すると、逐次一貫性があるかのように実行される。非逐次一貫性をモデリングする必要があるなら、TLA+に明示的なロジックで書き下す必要があるが、手作業ではおそらく複雑すぎて間違いやすい。C/C++/Rustのメモリモデルは多くの奇妙なことを許容している。各変数に読み取りキャッシュとライトバックバッファを追加し、適切な箇所にキャッシュフラッシュ命令を入れる必要があるのだろうが、もっとエレガントな方法があるのかもしれない。
Rustを使うなら、miriとloomの両方に、非逐次一貫性のある動作をチェックできるアナライザーがある（そしてloomは実際には逐次一貫性を全く実装していない）。
- adamddev1
素晴らしい記事だ。人々は「テストを書けばいい」とか、最近では「形式検証を使えばいい」と言い続け、それで十分な安全策だと思って実装のすべてをLLMに丸投げしている。しかし実際には、確率的に推測する機械では彼らを救えない。人々は自分が作っているものを実際に理解する必要性から逃れられないのだ。
- rrook
これは我々のプログラミング言語の欠点の一部だと思う。一般的に、言語は部分グラフの表現を許すため、検証問題が技術的に難しくなる。私の見解では、閉グラフのセマンティクスのみを公開する言語は、たとえ絶対的でなくても、モデルと実装のギャップを埋めるのに役立つだろう。
- metabagel
インラインフットノートが最高！