最近Coqなどの証明系が流行ってると聞きました。これはポストHaskellと言うべき言語なんでしょうか。
それとも、別種の、実用言語ではなくて理論を突き詰めるためのものなんでしょうか。

アホな質問ですみません、Coqのサイトを少し見たのですがさっぱり分からなかったので。
よろしくお願いします。