search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 233 forks source link

Caching proof obligations #130

Closed catalin-hritcu closed 7 years ago

catalin-hritcu commented 9 years ago

I think we're starting to badly need caching of proof obligations. Otherwise too much human time is wasted on re-checking the same things over and over and over again, during an interactive proof.

We had formula caching in F5; maybe we can get some inspiration from there (discharge.fs in particular): https://www.infsec.cs.uni-saarland.de/projects/F5/browser#trunk/Typechecker I'm sure there are many other tools that do this too though.

catalin-hritcu commented 7 years ago

One can see hints as a smarter variant of proof obligation caching. Closing.