なぜ今，形式的手法か
形式的手法も1度，1980年代に日本で研究対象として注目を集めたことがある。しかし，当時はまだソフトウエアの規模自体が膨大ではなかった上，ソフトウエアの上流工程の重要さもあまり実感されていなかったことから，その後，研究は下火になった（図7）。日本における形式的手法の第一人者である九州大学大学院 システム情報科学研究院 情報工学部門 教授の荒木啓二郎氏はこう語る。「1980年代はソフトウエアのモジュール化が有効との議論がなされていたような時代。今ではモジュール化は当たり前のこととして現場に定着し，誰もそんなことは議論しなくなった。当時，形式的手法を現場に適用するのはあまりに早すぎたのかもしれない」。
形式的手法とは別に米国などでソフトウエア工学の研究が進み，数々のソフトウエア開発プロジェクトの失敗事例が積み重なったことで，上流工程を重視した方が結果的に効率が良いことが経験的に判明してきた今，再び形式的手法の実践に正面から取り組むべき時期が来たといえる。
ただし，形式的手法が1970年代に欧州で誕生し，数十年の歴史を持つにもかかわらず，日本では全くといっていいほど現場に導入されていない。「形式的手法は数学の知識を要し，難しすぎるから使えない」という偏見があるのも事実である。
形式的手法を実践する際の困難さは，手法そのものにあるのではない。便利で役に立つシステムを作ろうとする際の本質的な難しさに，形式的手法を介して向き合っているだけである（図8）。同様の困難さはオブジェクト指向分析にも存在する。形式的手法が他の手法と異なるのは，モノづくりに潜む本質的な難しさに「仕様精査という早い段階から向き合うよう示唆している点くらい」（産業技術総合研究所 システム検証研究センター 副研究センター長の高橋孝一氏）であろう。早い段階でそうした問題に向き合うからこそ，多少の苦労も伴うが同時に効能も大きいのである注5）。
注5）形式的手法は数学の論理学に基盤を置き，集合論の記号などを一部用いている。一見してなじみのない記号が並ぶため，非常に数学的で難しいという印象を与えてしまう面はある。しかし，形式的手法を経験したエンジニアの多くが，そうした記号の多くは数日の座学を経れば，難なく理解できるようになると語る。形式的手法で厳密な仕様を論理的に精査するには，モノづくりの本質的な難しさと向き合う必要があり困難を伴うものの，形式的記述言語で書かれた仕様を読むだけであれば，通常のプログラミング言語の構文を覚える作業と何ら変わらない。仕様を読む個人による解釈の差を減らす目的であれば，導入に伴う障害はあまりないといえる。
