"失敗を美しくする。それが設計の責任だ。"
バグを「実行時に捕まえればよい」と考える設計では、誤りはいつか現実となる。
Adaは、その発想を根底から否定する。失敗は“動く前に”露呈させるべきだ。
そして、SPARK Adaが体現するのは、失敗を構文として設計に織り込む美学である。
失敗を「予測」ではなく「前提」として扱う
たとえば、次のコードを見てみよう。
function Safe_Square (X : Integer) return Integer
with
Pre => X <= 46340;
これは、「46340を超えるとオーバーフローする可能性がある」ことを、事前に宣言している。
これに違反するコードは、GNATproveがコンパイル時に契約違反として拒否する。
コンパイルとは検証の第一関門である
従来の言語では、コンパイラは構文と型しか見ない。
Ada／SPARKでは、意図・制約・関係性までもがコンパイル時に検証対象となる。
つまり、正しくない設計は、書いた時点で“止められる”世界がそこにある。
“失敗する”ことを恐れない——設計における覚悟
SPARKにおける契約は、「満たされているかもしれない」ではなく、
**「満たされていることを証明できなければならない」**という世界観。
この厳しさが、設計者に**「意図を記述する責任」**を負わせる。
実行前の拒絶＝設計の透明性を守る構造
function Divide (A, B : Integer) return Integer
with Pre => B /= 0;
このような関数が存在する場合、Divide(X, 0) はそもそも成立しないコードとなる。
これは、エラーハンドリングではなく、設計ルールの静的強制であり、
「後で直す」のではなく、**「最初に間違えられないようにする」**という思想である。
結語：失敗が“設計の余白”でなくなった世界
Ada／SPARKが示すのは、「ミスをしてはいけない」世界ではない。
むしろ、「ミスが起きる余地を、構文の段階で潰す」という設計による救済の哲学である。
失敗は隠さずに晒し、止められるべきである。
それを“設計としての構文”で実現する——その強さが、Adaの美学だ。
"止まるコードは、未来の破綻を防ぐ設計者の意思である。"