Geminiとこれを土台に議論したけど、Geminiは「形式検証って学習曲線がつらいかし、やっぱミッションクリティカル向けでは?」って反論してきて、
それに「むしろミッションクリティカルな環境以外ではオプショナルな導入で十分で『書きたい人が必要な部分にのみ』ってスタイルで良さそうだし、なにより形式検証によるエラーメッセージは初学者に対して優しいヒントになるんでは?><」ってなって、
Geminiが「たしかにそういう発想でのオプショナルな導入であればかなり有用だし、初学者のアシストとしての形式検証環境ってコンセプトは新しいかも!」(意訳)
ってなった><(実際はもっと長い議論です)