Hacker News new | ask | show | jobs
by jojo3000 4283 days ago
In interactive theorem proving HOL4 (http://hol.sourceforge.net/) and Isabelle (http://isabelle.in.tum.de/) are written in SML and are actively developed.