Re:Coq 8.6 is out
by mrefj on Tuesday December 27, 2016 @04:03PM
(#13266164)
> If you mean you want it to be automated
ACL2 is an alternative that strives to strike a balance between interaction and automation.
- It is more automated than any of the interactive theorem provers including Isabelle/HOL, Coq, etc.
- Its authors received the ACM software system award in 2005.
-It is used in commercial products since several years in companies including AMD, Centaur , Rockwell Collins, etc. There is a not-so comprehensive but yet impressive list of applications here:
- Also, since the language is a subset of Common-lisp, any one who knows a bit of programming can very quickly start using ACL2. One does not need to learn type theory/logical formalism to start using it. It has an eclipse plugin that is used by first and second year undergraduate students (http://acl2s.ccs.neu.edu/acl2s/doc/).
ACL2 is an alternative that strives to strike a balance between interaction and automation.
- It is more automated than any of the interactive theorem provers including Isabelle/HOL, Coq, etc.
- Its authors received the ACM software system award in 2005.
-It is used in commercial products since several years in companies including AMD, Centaur , Rockwell Collins, etc. There is a not-so comprehensive but yet impressive list of applications here:
http://www.cs.utexas.edu/users/moore/publications/acl2-paper...
- Also, since the language is a subset of Common-lisp, any one who knows a bit of programming can very quickly start using ACL2. One does not need to learn type theory/logical formalism to start using it. It has an eclipse plugin that is used by first and second year undergraduate students (http://acl2s.ccs.neu.edu/acl2s/doc/).