AIと共に進化する開発手法：形式手法と関数型プログラミングの可能性
物量の多さ: ガードレール がないと必要ないものもどんどん追加する コンテキスト の理解の限界: 複雑な依存関係や暗黙的な案件を完全に把握するのは困難 品質保証の新たな課題: よしなにやってくれるが、開発・改修が数年単位で積み重なった先にどうなるかは未知
上記のような問題点を 形式手法 を用いることで軽減できる 元来、形式手法を開発プロセスに組み込むことは導入面・運用面からコストが高かった
しかし、AI Agent の台頭により、このコストを軽減することが可能に
なぜ形式手法か？
自然言語 の曖昧さを排除: AI が進むべき道筋を明確に 完全性 の保証: すべての状態とケースを網羅的に記述可能 形式手法: 数学的に厳密な仕様記述
https://gyazo.com/2f52302c78a8d0eb211e87249eba7e77
Alloy 6 から 時相論理（線形時相論理）が導入されが、TLA+ ほどの表現力は無いのでそこは TLA+に委ねるってことなのかな？radish-miyazaki.icon そもそも TLA+ は時相論理ベース
2. 形式検証による問題発見
3. 統合的な制約明確化
構造的制約（Alloy で検証済み）
動的制約（TLA+ で検証済み）
統合制約（Alloy + TLA+ で検証済み）
4. 再度自然言語に落とし込む
https://gyazo.com/e3cbbe3a7b402f74569d4671c194a83a
なぜ ADT なのか
制約を型システムに直接埋め込むことができる
組み合わせることで複雑な制約を表現できる
関数型ドメインモデリング
不可能な状態を型で表現不可能にする（無効な状態を作れないようにする）
これにより人間だけでなく、AI によるコード生成時の助けにもなる
状態遷移の制約を型レベルで表現する
高度なテストパターン
AI 駆動開発の可能性: 究極的な レフトシフト を AI の力で加速できる https://gyazo.com/4fd51a659e7a2a6d51cc39f1a5cec400
人間が律速になってしまっている問題が更に深刻になるので、それを軽減できる