形式仕様言語
数学的な厳密さでソフトウェアの仕様を記述するための言語。自然言語の曖昧性を排除し、検証可能な形式で要求や設計を表現することを目指す。
代表的な言語
| 言語 | 特徴 |
|---|---|
| TLA+ | 並行システムの仕様記述。Leslie Lamport設計 |
| Alloy | 関係モデルに基づく軽量な形式手法 |
| Z notation | 集合論・述語論理ベースの仕様記述 |
| VDM | Vienna Development Method。モデルベースの形式手法 |
普及しなかった理由
歴史的に学習コストの高さと実用性のギャップが障壁となった。仕様と実装が別のアーティファクトになるため二重管理問題（SSoTの不在）も生じる。
仕様と実装の統合を目指すアプローチ
形式仕様言語の理想を、実行可能なコードの中で部分的に実現するアプローチがある。
- 依存型言語（Idris、Agda）— 型レベルで不変条件を表現可能。「長さNのリスト」のような仕様が型に埋め込まれる
- 篩型（Refinement Types）（Liquid Haskell、F*）— 既存の型に述語を付加し、
{x: Int | x > 0}のように制約を型に乗せる - 契約による設計（Eiffel、Ada/SPARK）— 事前条件・事後条件・不変条件が言語レベルでサポートされる
現在では判別共用体やRustの代数的データ型が、より軽量にこの役割を部分的に担っている。型駆動開発も同じ方向性にある。
表現力と学習コストのトレードオフ
仕様記述言語が実用的に成立するには表現力と学習コストの両立が必要だが、表現力を上げれば学習コストが上がり、学習コストを下げれば既存のプログラミング言語と大差なくなるという本質的なトレードオフがある。
ただしAIが変換を担う世界では、言語自体は読みやすくさえあれば書きやすさの重要性が下がるため、このトレードオフが変わる可能性がある。