3 ms·
> the solution for this But what is "this"? I think the only criticism of existing theorem provers at https://practal.com https://practal.com is that Coq uses
by creata 5y ago
> the solution for this
But what is "this"? I think the only criticism of existing theorem provers at https://practal.com https://practal.com is that Coq uses coercions rather than subtyping. Is there a practical example where Coq just doesn't have a good equivalent for what subtypes can do?
- auggierose 5y agoCoercions / subtyping is a big one, because mathematics is full of quotient types and identifications. This is a very practical issue, that comes up many many times. Not necessarily if you "program" in Coq, but if you try to do math in Coq. Another one is that there is no good treatment of undefinedness. An "option" type doesn't cut it, because it pollutes everything. The question is, how can you enable undefinedness everywhere, without polluting everything? That is only possible by adjusting your logic.
- creata 5y agoThis is a very late response, but thanks, those all seem like great reasons.