Hacker News Reader

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