3 ms·
> It is also possible, to some extent, to use dependent types to replace proof tools like Coq. Not sure what you mean here - Coq is a proof tool _based on_ dep
by wk_end 4y ago
> It is also possible, to some extent, to use dependent types to replace proof tools like Coq.
Not sure what you mean here - Coq is a proof tool _based on_ dependent types. It's a dependently typed programming language with a mechanism for constructing proof terms in an (arguably) more pleasant or natural way bolted on top.
- Jtsummers 4y agoThey probably mean that bringing dependent types into a programming language, proper, partially obviates the need for Coq and similar systems since it renders them (at least partially) redundant. Having dependent types, and having mechanics in-language to produce proofs, would cover a large part of what people (who are producing programs and not focused strictly on the theorem proving side for other purposes) are using Coq & others for.