形式手法 - 角谷鵜技術五十三次

形式手法

定理証明は昔からあるのにあんまり普及してないのはツールの問題があるんじゃないかと思ってます。すなわち、プログラムを書いてるときに「あ、この部分証明できそう」と思ったら一旦そのプログラムを定理証明支援系に移植して証明してExtractするのが面倒すぎるのです。

普段から定理証明支援系でプログラムを書けばいいじゃん

それで問題ないならいいんですが、定理証明支援系ってプログラムを書くのにそんなに便利じゃなくないですか？

私が想定している証明の使い方は、普通にプログラムを書いて、普通にテストして、特に重要そうな部分は証明つけよっかってなるフローです。

依存型のあるプログラミング言語と定理証明支援系の本質的違いはない

構文や標準ライブラリの設計、利用者層の違いがあります。

特に、依存型はプログラムのパーツとしても便利なので何の気なしにプログラムを書いていたらうっかり足を滑らして定理証明をはじめてしまえるのもポイントですね。