僕の所属する研究室では毎年Software Foundationsの輪講をやっているんですが，Brzozowski derivativeに基づいて正規表現エンジンを実装し，あまつさえCoqで検証してしまおうといった練習問題が追加されていて大変興味深かったです． 折角practicalなプログ…