We don't have a formal result on this yet, but my belief is that under certain circumstances changes to a proof only require a small subsection of the final proof terms to be rerun. For example,
if we change a Hoare triple, we should be able to invalidate only the proof terms coming from that Hoare triple and re-run them;
if we change a view constraint, we should be able to invalidate only proof terms involving superviews of that view constraint as a precondition, postcondition, or goal, but this is a bit more subtle.
In this case, we should make Starling more amenable to running only small bits of the proof, for example for inference testing. See also #143 and #144.
Another possibility this could open up is, when we run Starling, we could store a hash of Starling elements (axioms, terms, etc.) alongside their results, and then allow 'quick proofs' that compare the proof outline against those and generate only proof terms for things that have actually been invalidated. This is maybe best left as a hypothetical for now.
We don't have a formal result on this yet, but my belief is that under certain circumstances changes to a proof only require a small subsection of the final proof terms to be rerun. For example,
In this case, we should make Starling more amenable to running only small bits of the proof, for example for inference testing. See also #143 and #144.
Another possibility this could open up is, when we run Starling, we could store a hash of Starling elements (axioms, terms, etc.) alongside their results, and then allow 'quick proofs' that compare the proof outline against those and generate only proof terms for things that have actually been invalidated. This is maybe best left as a hypothetical for now.