形式手法はなぜ流行っていないのか - Qiita

はじめに みなさん形式手法をご存知でしょうか？ 名前くらいは聞いたことあるけどいまいち何かわからないという方が多いのではないでしょうか。 その通りです。形式手法はアカデミアではそれなりに研究されているものの、 一般の（特にWeb系）ソフトウェア開発者が携わることはなかなかないのではないかと思います。 この記事ではソフトウェア開発に形式手法が導入されないのはなぜなのかを考察します。 この記事ではアジャイルソフトウェア開発において形式手法を導入する際のハードルについて考察します。 追記 本記事について、「形式手法は流行っていない」というのは正確ではないのではないかという指摘をいただきました。組み込み系や社会インフラ系等バグを絶対に出せないシステム開発では形式手法がよく使われているそうです。 ちょっと古いデータですが活用事例です。 誤解を招く紹介となっていたことをお詫びします。 さらに追記 ku

[uzusayuu]

ちなみに半導体回路の設計ではフォーマル検証はごく一般的なツール。 ただ使われ方がだいぶ違う。（HDLからネットリストとかで使う）

[jt_noSke]

流行ってないというか、使ってるところが航空・鉄道・電力とかバグったらヤバいところでいろいろ採用されてるという話を聞くけども

[turanukimaru]

ユーザと開発者がシステムを完全に理解し未来も完全に予測し記述も完全にできれば、形式手法は完全に機能する。問題はもちろん、それがなんであれシステムを完全に理解している人間などいないという事だ。

[tanakakazu]

静的型の言語でさえ「めんどくさい」「たいへん」「気持ちよく書けない」とか言う人いるしね。

[mayumayu_nimolove]

手段を流行らすのは形式的におかしいんだよ。目的を叶える手段が流行る。目的ありき。

[kamocyc]

頭に「Web系では」って付けてほしいと思う(といっても他の業界はよく知らないが)

[kirakking]

実用性は把握していないけど Isabell/HOL もコード抽出ができるみたい "Code generation from Isabelle/HOL theories" 。検証フレームワークを体系的に学ぶのではなく言語レベルでの制約(Rust のメモリ安全等)がこれから流行るのではと思う

[georgenano]

軽量な形式手法である型検査はめちゃ流行ってるじゃん 流行ってないところを形式手法と呼んでるだけな気がする AIと一緒。実用的になると専門の名前をつけられてAIって呼ばれなくなる。

[suzuki_kuzilla]

手形決済に空目した。疲れてる

[findup]

組み込みやってるときには割と聞いた。Webとかアジャイルとは相性悪いでしょう。IT業界＝Webみたいな感覚だとなかなか聞かない話かと。

[simomm]

形式手法とは高い信頼性が必要なソフトフェアでは使われるらしい。

[burabura117]

“実は形式手法はAIと同じように実用的になった時点で別の名前がつく言葉なのかもしれません。”

[ytakano]

Rust流行ってるやん

[rryu]

形式手法はより厳密にプログラムを書いている感が強くてプログラミング言語側でなんとかならないものかと思っていたが、確かに最近よく見る厳密に型を定義する手法がそれっぽいかもしれない。

[prjpn]

構成の変更が生じたとき陳腐化する定め

[kobito19]

費用対効果に尽きるのでは

[tettekete37564]

知らんけどフローチャートやUML図はまあまあ書くよ。若手にはバカにする連中もいるが、認識のすり合わせやカバレッジ洗い出すにはなんだかんだで重宝する

[morita_non]

銀行その他の業務を形式化するのが先か。Coq楽しいんだけど。

[terazzo]

普段我々は自分の能力を超えたものを作ってるんだと思う

[NOV1975]

主にコストの問題なので、コストより品質が重要な分野では使われている、のではないかな。

[alt-native]

その昔 同期が形式手法やってた。開発者だらけの社内でも形式手法の理解者は少なかった。運用できるようになるまでに結構コストかかるんだよね。

[kura-2]

全部で適用するだけの理由がないからじゃないの？こういうのよくあるが、ほんとに全部に適用して流行るとみんな幸せと思ってんのだろうか？ということで、タイトル変えると読むタイプの記事

[delphinus35]

面白かった。いいオチまでついててよかった。

[SWIMATH2]

話の展開が上手くてほーとなった

[qtamaki]

定理証明では公理が正しい事を証明できないから？

[roshi]

確かにユニットテストは最初知った時なるほどなーと思った。あの時と同じような体験をできる程度に平易な形になったら普及しそう。

[saiyu99sp]

“False alarm”これされてマジでムカついた。

[megamouth]

“開発者体験”

[t-tanaka]

TCPスタックでもWebサーバーでも何でも良いから，実用的なものを実装してくれ。それができたら考える。

[ngmy]

流行らない理由は、証明検査系自体や記述した仕様自体にバグがあった場合のダメージが大きすぎるからでしょうね。