4 ms·
Incorrect: ACL2, an industry-standard automated theorem-prover, is written in a side-effect-free variant of Common Lisp. It has both an implementation and users
by lmkg 17y ago
Incorrect: ACL2, an industry-standard automated theorem-prover, is written in a side-effect-free variant of Common Lisp. It has both an implementation and users, including users outside of academia.
http://en.wikipedia.org/wiki/ACL2 http://en.wikipedia.org/wiki/ACL2
- moe 17y agoI guess both (no implementations, no users) were meant in relative terms, and in that light they describe reality pretty well. Hands up, who has heard of ACL2 before?
- rbanffy 17y agoI did. In fact, I am appalled so few people, apparently, heard of it.
- jrockway 17y agoAny programming language that can't be cut-n-pasted from fifty different websites to make my SQL-injection-rich AJAX social awesome NoSQL site just isn't worth knowing. Theorem proving -- you ain't gonna need it! What's next, you're going to tell me you write unit tests? Hahahahah.
- rbanffy 17y agoIn theory, at least, I wouldn't need them for I proof the program is correct ;-)
- sigstoat 17y agome. i've even used similar tools.