私はCoqでコードを記述し、このコードを抽出して大規模なHaskellプロジェクトで使用することを検討しています。Coqで単一のモジュールを構築し、プロパティを証明してから、Haskellのモジュールシステムを使用して、これらのプロパティの違反を（スマートコンストラクターを介して）防止したいと思います。
明示的なエクスポートリストを使用してCoqコードをHaskellモジュールに抽出できるという兆候は見つかりません。抽出されたCoqコードを手動で変更する必要があるようです。これは大したことではありませんが、この権利があるかどうかを知りたいと思います。誰か別の提案がありますか？