"コードが設計者の意図を語れるなら、対話すべきは人間ではなく構造である。"
かつて、コードは人間が読めるものではなかった。
その後、プログラミング言語は読み書きの対象となり、「わかりやすさ」や「表現力」が求められるようになった。
しかしSPARK Adaが示すのは、その次のフェーズだ。
コードが自ら設計意図を“証明し、保証し、主張する”世界である。
本稿では、形式手法時代における「人間とコードの新たな関係性」について掘り下げる。
設計意図をコードに埋め込むという転換
function Transfer (From, To : in out Account; Amount : Positive)
with
Pre => From.Balance >= Amount,
Post => From.Balance = From'Old.Balance - Amount and
To.Balance = To'Old.Balance + Amount;
これは単なる“関数”ではない。設計文書であり、制約の宣言であり、証明可能な設計仕様である。
つまり、コードが仕様を語り、検証者に説明責任を果たす存在となっている。
会話の相手が人間ではなくツールになる世界
SPARKでは、設計レビューの対象が人間の目視チェックではなく、
静的検証ツール（GNATprove）との対話となる。
- 仕様通りか？
- 契約は破られていないか？
- 未定義な振る舞いがないか？
これらを人間が推測する必要はなく、機械が証明し、コードが語る。
ドキュメントが不要になる構造的誠実さ
SPARKにおいて、仕様書はコードに吸収される。
Pre/Post、型制約、不変条件など、設計情報が構文そのものに宿るためだ。
結果として、文書とコードが乖離することがなくなる。
“設計者が何を意図したか”がコード自身に語らせることができる。
人間の責任が「書くこと」から「意図を設計すること」へ
従来の開発では「正しく書く」ことが主な責任だった。
SPARKでは、「何が正しいのかを定義すること」が責任となる。
これは、プログラマの役割が実装者から“制約を設計する存在”へ変化することを意味している。
結語：設計とは、人が語るのではなく、構造が語るものへ
機械は嘘をつかない。だが、曖昧な構造は真実を語らない。
SPARKは、コードを「沈黙する命令列」から、設計意図を語る構造体へと進化させる。
人間の仕事は、仕様を紙に書くことではない。
それをコードに語らせるための設計構文を選ぶことなのだ。
"人が語る設計には限界がある。構造が語る設計こそが、次の開発の礎である。"