8月はちょっと纏まった時間がとれたので、
「ソフトウェアの基礎」日本語訳の練習問題を解きすすめてみた。

まだPoly.vが終わった序盤だけどだいぶCoqに慣れてきた。
星三つrecommendedでもたまに難しい問題があるなー、というのが感想。

論理学の命題というのは高校・大学教育で慣れているだけで
見直してみると思ったよりも複雑な構造をしていたのだと今更ながらに感じた。

実務でCoqが要求されることは当分ないと思うけど、
逆変換の関数は少なからず実装することがあるので
ときどき「Coｑ使って証明したい」という気分にはなるんだよなー。