"信頼とは、意図と構造が一致しているという一点に宿る。"
全30本に渡って見てきたAda／SPARKの思想と実装。
最後に改めて問いたい。
「私たちは、何をもってコードを信頼していたのか？」
Adaは、設計とは何かを定義し直す。
それは、コードの速さでも、柔軟さでも、見た目でもなく、
「その構造が、どこまで未来を約束できるか」という一点に集約される。
信頼とは、バグが起きなかった実績ではない
多くの現場では、こう語られる：
- バグが出なかったから安全
- テストが通っているから安心
- たくさんのユーザーが使っているから信頼できる
しかしAdaは、もっと冷徹にこう問いかける：
「それは“偶然動いた”だけではないのか？」
信頼性の新定義：予測、制約、検証、証明
Ada／SPARKが示した信頼性の条件は、こうである：
- 予測可能であること（非決定性の排除）
- 設計意図が構文で表現されていること（契約）
- 機械的に検証できること（静的解析）
- 証明可能であること（数学的保証）
これらが揃って初めて、「これは信頼できる設計だ」と言える。
開発者に問われるのは、「何を選ぶか」ではなく、「何を許さないか」
Adaを使うことは、あらゆる選択肢を狭めることであり、
それは裏を返せば、曖昧さと不安定さを“許さない姿勢”の表明である。
この構造を選んだ時、私たちは「自由」を捨てたのではない。
“守るべき信頼”のために、必要のない自由を放棄したのだ。
曖昧を語らず、正しさを語るコードへ
Adaのコードは、どれだけ書いても饒舌にならない。
ただそこに在り、構造で語る。
それは設計者の思想の断面であり、責任の形式知であり、未来への構造的遺言だ。
結語：構文に宿る信頼、それがAdaという思想
この30本を通じて見えてきたのは、
Adaという言語が単なるツールではなく、
設計者の“信頼されたいという意思”を受け止める器であったという事実である。
私たちは、自由に書くこともできる。
しかしその先に「正しく設計された構造」がないなら、信頼は生まれない。
Adaは言う。
"書けるコードより、信じられる構造を残せ。"