Coq言語に勢いを感じる

Coqについて検索してみると、面白い研究がなされているようです。

Coqは自動証明ができるプログラム言語で以前から興味がありましたが、改めて注目したい言語のようです。

既に、Haskellの抽出可能なようです。何故変換という言葉を使わないのか疑問に感じ少し調べてみましたが、多分ロジックの意味のある部分だけのコードを抽出するようです。

自分は以前からDSLやPrologでプログラム変換を思考してきたので、Coqでも同様のことが行えるので期待できる手法だと強く感じました。