契約プログラミングが使えることがすごいわけじゃなくて、『契約プログラミングで安全を数学的に証明できるようにコーディングしないと警告が出る環境』だから失敗したら人が死ぬ分野でも使える環境って、なるほどだし、
SPARKが無かった頃のAdaによる実装で起きたAriane 5の最初の打ち上げでの打ち上げ失敗（クラスターミッション）みたいなのを防げる技術なのか＞＜

クラスターミッション - Wikipedia
https://ja.wikipedia.org/wiki/%E3%82%AF%E3%83%A9%E3%82%B9%E3%82%BF%E3%83%BC%E3%83%9F%E3%83%83%E3%82%B7%E3%83%A7%E3%83%B3