I know. But if not even professional programmers use Coq day to day (because it's hard to use, the limitations and well known, etc.) why should we base our laws

I know. But if not even professional programmers use Coq day to day (because it's hard to use, the limitations and well known, etc.) why should we base our laws on it? WE should start using it, when we enough gain experience we start using it in law writing. As a matter of fact I'm going to check out Coq right now...