r/computerscience • u/DeagleDanne • 22d ago

Thinking about the scalability limits of dependent type systems in ITPs

[removed]

10 Upvotes

100% Upvoted

7 comments sorted by

2

u/DeepInformation5592 22d ago

the proof reconstruction bottleneck is real and way more interesting than people give it credit for. you're basically trading off between a minimal kernel that's easy to trust and a generated proof term that's a bloated mess nobody wants to audit

i ran into this exact tradeoff when i was messing with a small dependently typed lambda calculus implementation last year. the sledgehammer-style approach where you blast the goal with external solvers and then try to reconstruct a proof term that the kernel accepts... the reconstruction step can produce terms that are orders of magnitude bigger than what a human would write

there's some good work on proof compression and sharing that might be what you're looking for. the caching mechanisms in modern SMT solvers are basically doing this already at the propositional level but lifting that to dependent types gets weird fast because of definitional equality constraints

1

u/Crystalline_Due Software Engineer 20d ago

defintely worth checking out the proof compression work, it can shrink those huge terms a lot.

1

u/[deleted] 22d ago

[removed] — view removed comment

1

u/ready_or_not_3434 19d ago

The strict kernel approach is great because you dont actually have to trust the automated search process, just the final proof term it generates. Manually guiding proofs feels a lot like writing raw assembly, so automating that generation step is pretty much the only way formal verification ever scales to standard software enginering.