形式手法が気になっている

2026年8月20日

最近、形式手法が気になっている。Quint とか TLA+ みたいなやつだ。

なぜ気になっているのかは自分でもよくわからないが、たぶん対比になっている。Python だと型で縛れないのが不便で、静的型付き言語を使いたくなる。それと同じで、自然言語で指示すると成果物がブレるので、形式手法で検証させる形で作業させたくなる。動的と静的の対比が、自然言語と形式仕様の対比として繰り返されている気がする。

問題は、職務範囲的にデータエンジニアなので、活用する機会があまりなさそうなことだ。Alloy はデータモデリングに向いているらしいので、触るならそこからかもしれない。