形式的検証

形式的検証ツールはいくつかある。

どれも微妙に用途が異なる。分散システムの検証ならTLA+が都合よく、もっとロジックに近い検証が必要ならLeanやDafnyが使えるらしい。

人間が書く場合は大量の記述が必要になるので現実的ではなかったが、AIエージェントを使うなら記述量は問題になりづらく、確率的に生成したコードの検証もテストコードより厳密に行えるので便利なのかもしれない。

RussがBlueskyで以下の記事をリポストしていたので、LLMの登場によってプログラミング言語は変わるのかで話題にしていた「抽象度が上がる」の方向性はこっちなのだろうか。