「仕様書は存在しない」——形式手法の限界と可能性
Specifications Don't Exist (2025)
形式手法の成功例は、コンパイラや暗号ライブラリ、マイクロカーネルなど、自然に形式化できるシステムに限られています。しかし、WebブラウザやPDFのような複雑なシステムには、正確で一貫性のある形式的仕様を書くことはほぼ不可能です。本記事では、Galoisの経験から、仕様書が存在しない理由と、形式手法の適用範囲について考察します。
PDFは存在しない、少なくとも形式化できる離散的なカテゴリーとしては。
HNでの議論
13- ivanbakel
仕様書作成に関する非常に正当な見解だ。形式検証の研究は、まるで酔っ払いが街灯の下で鍵を探すようなものだと感じることがある。というのも、対象となる領域は往々にして、特定の種類のコンピュータサイエンスを適用するのに適したものだからだ。
しかし、『自然に検証可能な』領域と難しいケースの間には中間領域があると思う。銀行アプリのような特定の領域では、UIの動作に関する正確性の保証が求められることがある。閉じたアプリは非常に規範的であり得るので、理論上は『ユーザーがこのアクションを実行し、それを確認した』といった仕様を意味のあるものにできる。しかし、仕様をUIに結びつけるのは厄介な問題であり、関数の境界がそうであるようには、明らかに不安定だ。アプリは再設計され、スタイルや要素は移動する。UIを状態機械として抽象化することは想像するのは難しくないが、実際に仕様をプログラムに結びつけることはそれ自体が問題であり、一般的な対応は、こうした問題のある領域を無視して、PLの形をしていない疑問に対処する必要のないバックエンド仕様のような、より簡単なことを行うことだ。
- mad44
現在、Speculaのようなプロジェクトがあり、LLMを使用して実装から仕様を導き出し、逆説的ではあるが、その仕様を使用して実装のバグを見つけることができる。
https://muratbuffalo.blogspot.com/2026/08/specula-scaling-fo...
第二に、オープンな部分仕様や合成可能な仕様は、Doddが引用しているモノリシックな仕様の問題に対処するのに役立つと思う。
https://muratbuffalo.blogspot.com/2026/08/composition-and-mo...
- tel
ここ数ヶ月、Markdownに似た軽量ドキュメントフォーマットに取り組んでいる。（簡単に言うと、Markdownに似ているが、自然な拡張ポイントが組み込まれており、はるかに曖昧さが少ない。）
私の目標の大きな部分は、このフォーマットの『仕様書』を書くことだ。ユーザーが私の主要な実装に対して、仕様に従っていないというバグを正当に報告できるほど、良いものにしたい。それが言語についての真実の源だからだ。
だから当然、『まあ、これで正しいかもしれない』というグレーゾーンについて議論するのはとても興味深い。このプロセス全体が、私に次のことを促している。(a) 言語自体を弾力的で寛容なものにし、ほぼすべてのドキュメントに対して何らかの答えを持たせること、(b) システムの出力を制約して、できるだけ多くの情報を捨てるようにし、意味論についてより自信を持って主張できるようにすること。
目標をすべて達成できるかどうかはわからない。これは小さなプロジェクトであり、ウェブブラウザなどよりはるかに単純だ。同時に、私が本当にそのような仕様に何を言ってほしいのかを絞り込むのは非常に難しい。