Ada/SPARK環境、なんか単に契約プログラミングで自動的に安全にしてくれるような環境を想像してたけど、
どっちかというと、数学的に証明不可能になってる数学的に曖昧な記述の個所を検査機(gnatprobe)が見つけ出して、契約プログラミングの記述で条件を指定して数学の証明の文脈で安全性を確保できるコードに書き換えさせる環境みたいな感じなのか・・・＞＜