Post #2101897
2026-05-02 17:56 UTC
@jonmsterling Do you think it is possible to make an ML/prover combo in the LCF style so that the metalanguage’s module/locale/… system can adequately model mathematical hierarchies, or is the pure LCF architecture relegated to history?
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-05-02 18:01
@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.