Wanted: partial evaluation and staging for proof search.
And I don't mean the idealized proof search of a logic, but the one from a proof assistant, and one supporting domain-specific proof automation.
Conversation
Yes me too! That would be so neat.
1
1
I mainly want this for dependently typed metaprogramming, levitation, and faster codegen, but yeah, having it for proofs would be really cool too.
1
OTOH...
"I want staging"
Mom: "we have staging at home"
Staging at home: Coq's "Eval cbv in <term>"
1
2
"I want staging"
Mum: "we have staging at home"
Staging at home: `const fn foo<const x: Int>() -> T { ... }`
1
2
not sure I get what staging means here? would you mind explaining? 😅
1
(I have a metaprogramming project going at $dayjob and if it's a concept I'm not familiar with, I'd like to know more)
1
TBH I need to understand more about it, but here I think you can consider it's a bit of code that is 'staged'. ie. it won't be compiled until you provide it with a constant argument.
1
I do believe there might be a connection between 'staged programming' and Rust's 'angle bracket' parameters (which are always monomorphised), but I'm not really sure of the precise connection. There's a bibliography of related stuff here:
3
1
1
Have you heard the good word of Pfenning-Davies S4? cs.cmu.edu/~fp/papers/jac
2
3
Yeah seen that one before… I should look at it again 😅