プログラムの正しさの証明をやりたいときは構造化言語のほうが
圧倒的に優れていると思う。