I'm surprised none of the Acorn documentation I can find mentions any of the existing declarative-style theorem provers, like Isabelle/Isar? This seems basically like one of those but with implicit proof search, and Isabelle/HOL's automation capabilities are quite powerful already. If Acorn is the future, it doesn't look like it's doing much to push the boundaries of the present.
prettiestmf@reddit
I'm surprised none of the Acorn documentation I can find mentions any of the existing declarative-style theorem provers, like Isabelle/Isar? This seems basically like one of those but with implicit proof search, and Isabelle/HOL's automation capabilities are quite powerful already. If Acorn is the future, it doesn't look like it's doing much to push the boundaries of the present.