Skip to content

Instantly share code, notes, and snippets.

@edwinb

edwinb/comment

Created July 19, 2014 00:11
Show Gist options
  • Save edwinb/5bc799f72f8199b260c1 to your computer and use it in GitHub Desktop.
Save edwinb/5bc799f72f8199b260c1 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
comment
I can’t help but feel that this is a really misguided effort.
When you start programming with dependent types, as your types get more descriptive you will inevitably end up needing to prove things. Hence, ultimately you will want the system to fulfill the role of a proof assistant, anyway.
It makes no sense, then, to dismiss Coq on the grounds that it is a proof assistant. Yes, it could use some facilities to make it more practical for actual programs. But it is a very mature system, based on a nice rich calculus, with lots of nice infrastructure, a growing standard library, lots of documentation and publications, etc. It makes much more sense to find out what Coq is missing and add it, rather than starting from scratch.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment