フォロー
なんで、AdaでしかSPARKというか、契約プログラミングを土台にした形式検証プログラミングが全く流行らないんだろう・・・＞＜
C#とか構文的にも静的検査の環境が充実してる点でも向いてるだろうし、Rustとかの安全を売りにしてる環境向けにもあってよさそうなのに＞＜
10年前とかのプログラマが使うPCでは、契約プログラミングの検査は遅かったけど、いま時のPCなら全然遅くないし、昔と違ってコード記述中にIDEがバックグラウンドで構文検査するのが当たり前になりつつあるわけだから、静的検査の時間によるストレスもほぼ無いだろうし・・・＞＜
Geminiとこれを土台に議論したけど、Geminiは「形式検証って学習曲線がつらいかし、やっぱミッションクリティカル向けでは？」って反論してきて、
それに「むしろミッションクリティカルな環境以外ではオプショナルな導入で十分で『書きたい人が必要な部分にのみ』ってスタイルで良さそうだし、なにより形式検証によるエラーメッセージは初学者に対して優しいヒントになるんでは？＞＜」ってなって、
Geminiが「たしかにそういう発想でのオプショナルな導入であればかなり有用だし、初学者のアシストとしての形式検証環境ってコンセプトは新しいかも！」(意訳)
ってなった＞＜(実際はもっと長い議論です)