4 ms·

I worked with Nqthm and ACL2. They seem best adapted to hardware verification. LEAN is pushing the edge of undergrad mathematics.

• lispm 3y ago
  "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?
• medo-bear 3y ago
  Thanks, I wasnt aware of the differences between various provers.