序
この記事、ちょっと、というかかなり感覚が古くね？ qiita.com
と思っていたら、炎上目的だったようで。
autotaker on Twitter: "「形式手法はなぜ流行っていないのか？」という記事を書いて炎上させたい"
autotaker on Twitter: "形式手法をこき下ろすと見せかけて最終的に出身研究室のステマに成功した"
一連の言い訳も見苦しい。
autotaker (@autotaker1984) | Twitter
故意に不正確な情報をばら撒く形でしか自分の"小さな得意分野"をアピールできないとは、エンジニアとして不誠実極まりないし、ミジメだ。
本題
ということで。
形式手法は80年代から本格的に開発が始まっているが、最初に大規模に報道されたのは90年代のIntelの不動小数点ユニットのバグ対策に形式手法が導入された件だろう。
つまりチップレベルでの導入。それ以前は鉄道や原子力など。ついで組み込み分野、そして現在は分散システム系。 基本的に形式手法は導入にコストがかかるため、それがペイする分野から導入が進んでいるということ。 (自分の目の前の状況だけで全体を判断すると、痛い目に遭う。)
10年前までの状況はこちらを参照 :形式手法適用事例の紹介
日本での例を挙げれば、JAXAの筑波側では積極的に形式手法を使ってるし、自動車分野もトヨタのUSAでのリコール問題をきっかけに本格的に使っている。
因みにトヨタのブレーキに問題がなかったことを証明したのも形式手法(のツールSPIN)だった。 システムが安全とは何か考える 〜トヨタ急加速問題のNASA分析を題材にして
上記のように、以前は組み込み分野が主だったが、現在は分散処理系での使用が活発。AWSでは10年前から積極的に使っていたし、 AWSにおける形式手法 分散DBでは当然のように使っている。たとえば、CockroachDBの これ やPostgresProのこれなど。
もちろん、形式手法があっても完璧なプログラムができるわけではないが、そもそもそれは考え違いで、たとえば建築CADがあるからといって完璧な建造物が作れるわけではないのと同様、形式手法は人間が手に負えない処理を補助するツールであって、完璧なプログラムをつくる魔法ではない。 だから普通に作れるレベルの複雑さのプログラムに形式手法は不要で、手に負えない複雑さをもつシステムに立ち向かうためのツールである。
(というか、大上段に構えずに、使えるものはなんでも使ってみればいいじゃん。なんでこうも保守的なんだろうね? )
余談
10年前にこれからは分散処理系でもモデル検証や形式手法が必要になると思って試したことがある。今となっては正しいモデル化かどうか疑問だが。 interdb.hatenablog.com
もともとspinは使っていたし、今でも個人的に使う。手法でありツールなんだから必要なときに使えばいい。
あまり知られていないだけで、複数の有償ソフトウエア会社が商売になるほどの市場もある。
個人的な印象だが、形式手法といってもいろいろあり、Intelのハードウエアレベルの検証のように大成功しているものもあれば、組み込みシステムのように比較的限定された機能の検証で成果がでているものもある。最近のAWSをはじめとする分散システムの検証も成功例になるだろう。
これらの成功例は、結局のところ、元々の問題(検証しようとしている事象など)自体が数学的なモデルに落とし込みやすいものだったといえると思う。回路ロジックしかり、分散システムならデッドロックやconsistencyなど数学的に定義できるものを対象としている。
一方、うまくいっていないものは、そもそも仕様を記述できていなかったり、定義自体が曖昧だったりと、まだまだ技術として適用できる段階に達していないようにみえる。
現時点では、うまくいっているものもダメなものもどちらも形式手法として一括りにされているため、ある人は形式手法は成功していると言い、別の人はダメな技術の典型にみえるのだろう。
私見だが、形式手法は主だった技術も理論も20年以上も前のものなので、本当の課題は現場のエンジニアがそれを使いこなすかどうかだと思っている。
その意味で、AWSがTLA+を使ったことはある種のブレークスルーだったと思う。数週間でマスターできると喧騒してくれたことが、形式手法を使うコストと心理的ハードルを劇的に下げた。
次の10年、適用分野がひろがっているとよいと思っている。
