Post #2236919
2026-05-02 18:01 UTC
@zwarich@hachyderm.io I mean, Isabelle does really well with this, and much of mathematics works fine with simple types. So I think pure LCF remains highly relevant.
I don’t think it is quite viable for dependent type theory, but I could imagine hybrid approaches.
Replies (1)
-
@zwarich@hachyderm.io 2026-05-02 18:18
@jonmsterling@mathstodon.xyz I don’t think of Isabelle as being a “pure” LCF prover, because it introduces its own syntax rather than relying on the metalanguage for user documents. This has obvious ergonomic benefits, but I am curious if different choices of metalanguage (and metaprogramming features) than the usual ones made by Poly/ML could improve the base experience so that Isabelle’s approach is unnecessary.