"沈黙はエラーがないことではない。証明された構造が、声を上げる必要を失ったのだ。"
テスト駆動開発、テスト自動化、CI/CD——
私たちは数十年にわたり、「壊れていないことを確認する」ための儀式を続けてきた。
だが、SPARK Adaはそこにまったく別の道を提示する。
**「テストしなくても正しさが保証される構造」**という、静かで強固な開発パラダイムだ。
テストとは「信じるしかない」行為である
テストとは本質的にサンプリングである。
ある入力に対して期待される出力が出ることを確認するが、それ以外は保証されない。
SPARKはその発想を根底から覆す。
すべての入力に対して、すべての仕様が守られることを証明する。
正しさが証明できる関数の例
function Max (A, B : Integer) return Integer
with
Post => Max'Result = (if A >= B then A else B);
このPost条件は、「Maxは必ず2値のうち大きい方を返す」という意味論的仕様である。
GNATproveがこれを通過するということは、Maxは“設計通り”であることが数学的に確定しているという意味になる。
テストは減り、設計が増える
テストが不要になるというのは、「確認しないでいい」ということではない。
それはむしろ、仕様と制約を構文として記述し、すべてを設計段階で検証するという意味である。
テストを書かないのではない。
テストの代わりに仕様を書く。
それがSPARKのスタイルだ。
テストから検証へ：静的保証の開発体験
- テスト：動かしてみる
- レビュー：人が読む
- デバッグ：バグを探す
→ SPARK：仕様を書く → 検証ツールが証明する → バグが存在できない
この静かな開発体験は、“壊れないことを証明する構造を設計する”という新しい美学である。
結語：沈黙は、正しさが語られる世界
動かしてみなくてもよい。
試してみなくてもよい。
テストを書かなくてもよい。
それは怠惰ではなく、証明によって沈黙を成立させた構造が、語る必要を失ったからである。
"コードが沈黙しているのは、語るべき矛盾が存在しないからだ。"