なぜデバッグが必要になるのか？

これらすべては、構文上・構造上で制御できない言語仕様から来ている。

SPARKが描く「バグが生まれない設計」

procedure Update_Score (Current : in out Integer)
  with
    Pre  => Current < 100,
    Post => Current = Current'Old + 1;

この構造において、100以上の値が入っていた場合、
GNATproveが“バグになる可能性”をコードを書いた時点で検出する。

デバッグではなく、証明によってエラーを封じる開発体験が実現する。

テストは「観測された範囲」しか保証しない。
だが、現実のシステムは観測しきれない分岐と状態を常に抱えている。

SPARKは、それら全てに対して、数学的に仕様を証明できる領域を提供する。
これによって、「たまたま通ったテスト」は**「常に正しい仕様」へと昇華される**。

それは「ラクができる」ということではない。
最初に設計と仕様を構文に刻むことで、後戻りを不要にするということである。

設計コストは上がる。だがその分、修正・障害対応・事故調査といった“開発の闇”をゼロに近づける。

デバッグとは、開発文化の一部であり、「仕方のないもの」とされてきた。
しかしSPARKは、その前提を構造ごと否定する。

「バグが生まれない」ではなく、「バグが生まれ得ない」。
その設計哲学が開発体験を根本から変える。

"直す前に、起こさせない。それが設計であり、証明の力だ。"