感想・レビュー
※以下の感想・レビューは、株式会社ドワンゴの提供する「読書メーター」によるものです。
mft
6
カリー・ハワード対応によれば、型は命題なので、プログラムは証明になる。ということで、自前で自然数を定義して色々な性質を証明し、負の数を含めた整数も定義して…というのを延々と続けていく。証明を完成させるタクティクというのがあってそれの使い方がいろいろ出てくるのが主な内容。結局プログラミング言語としてどういう感じなのかは全然見えなかった2025/09/15
Q
2
Leanという定理証明支援言語で性質を満たすことを証明しながら整数を自作する本。3章までで言語の基礎を手短に教えてくれるので写経しながら読んだ。Coqをあまり使いこんだわけではないので比較が難しいがVS CodeとLeanの組み合わせでの環境の使い易さに眩暈がしてしまった。exact?などのタクティクによって実際に適用される定理を探したりできるなど便利。Coqにもあるのだろうか？後半で自作整数を型クラスのインスタンスにするがこの行為によってどんな証明がしやすくなるのか説明があるとなお良かった。2025/12/22
