「形式手法はなぜ流行っていないのか」に対する異論 - interdb’s blog

序 この記事、ちょっと、というかかなり感覚が古くね？ qiita.com と思っていたら、炎上目的だったようで。 autotaker on Twitter: "「形式手法はなぜ流行っていないのか？」という記事を書いて炎上させたい" autotaker on Twitter: "形式手法をこき下ろすと見せかけて最終的に出身研究室のステマに成功した" 一連の言い訳も見苦しい。 autotaker (@autotaker1984) | Twitter 故意に不正確な情報をばら撒く形でしか自分の"小さな得意分野"をアピールできないとは、エンジニアとして不誠実極まりないし、ミジメだ。 本題 ということで。 形式手法は80年代から本格的に開発が始まっているが、最初に大規模に報道されたのは90年代のIntelの不動小数点ユニットのバグ対策に形式手法が導入された件だろう。 つまりチップレベルでの導入。それ

[grafi]

貴重な知見ですが、業界によるという話であんまり「異論」とは感じませんでした。たぶん、そういう業界に閉じていることが「流行っていない」と、炎上狙いを意識つつ呼ばれる理由なのかなと。

[devorgachem]

わかる