from Hacker News

Holbert: An Interactive Theorem Prover

by fennecs on 5/26/22, 5:50 AM with 9 comments

• by practal on 5/26/22, 8:12 AM

  > Unlike conventional theorem provers, Holbert’s term language is just the untyped lambda calculus. While this technically makes the logic unsound, it is much simpler to use as a pedagogical tool.

  I am not sure if it is very pedagogical to teach an unsound logic. How about you try a sound one? No types required: https://obua.com/publications/philosophy-of-abstraction-logi...

  I've come to the conclusion that Abstraction Logic (AL) is actually the golden middle between FOL (first-order logic) and HOL (simply-typed higher-order logic with Henkin semantics): You can view it both as FOL plus operators/general variable binding, and as HOL minus static types!