Hacker News Reader

Im not in this field so this might not be a good question, but why integration with LEAN and not ACL2, which is already written in Common Lisp

View on HN

I worked with Nqthm and ACL2. They seem best adapted to hardware verification.

LEAN is pushing the edge of undergrad mathematics.

"Faszinating" that a lot of these systems seem to be implemented from scratch in object-oriented C++ (?), instead of Prolog, SML, OCAML, Haskell, Lisp, ... what went wrong?

Thanks, I wasnt aware of the differences between various provers.

Reply on news.ycombinator.com