はじめに
形式手法という技術がなにやら面白そうですので、勉強してみたいと思います。
なんか面白いことができそう、ポテンシャル高そう、エッジな技術という印象です。
れっつら形式手法！
形式手法とは
数理論理学等に基づき品質の高いソフトウェアを効率よく開発するための科学的・系統的アプローチです。
- 明確で厳密
- 高い信頼性が期待
- 分析・検証が可能
- 導入コストが高い（と言われる）
[引用元] http://jasst.jp/symposium/jasst17tokyo/pdf/D3.pdf
なぜ形式手法か？
- 数理論理学を用いることで、明確で厳密なモデルを手にすることができる
- 明確で厳密であるため、自分の考えの推敲や他者との議論やコミュニーケーションが正確で効率的である
[引用元] http://jasst.jp/symposium/jasst17tokyo/pdf/D3.pdf
学習の動機
- 形式手法を使えば、ルールを使ったチェックや、ルールそのものの不整合をチェックしたりできるらしい。それってなんかすごくね？どんな感じでそれらがやれているのか、見てみたい。
- 形式手法はルールベースのお化けみたいな印象なので、これをAIのルールベースエンジンとして使えないかなー、みたいなアイデアを検証してみたい。ただし、汎用的な知的処理の仕組みとして使っていくことは難しそうだな、という印象はすでにあります。
- 仕事で使う（かもしれない）
とっかかりとして興味がある点、知りたい点
- どんな風にルールを実装するの？
- どんな風にチェックできるの？
- なんかすごそうなのに、ソフトウェア開発の現場であんまり使われていないのはなぜ？（複雑すぎる？コストが高すぎる？私が知らないだけで、ミッションクリティカルな領域では結構使われていたりする？）
- これ、業務で使えるの？（機能的に、ライセンス的に、難易度的に・・・など）
- AIのルールベースエンジンとして使える？
- 普通にチェックロジックを実装しちゃえばいいんじゃないの？