#11 ways of avoiding reproving

[Leo Freitas]

When specs get large, changes imply reproving. Reproving all is wasteful, if not prohibitive for productive work.
One solution is to separate zproof from z paragraphs. That is fine at the end, but not quite during development,
where you want to change and prove as you go along.

So, the tool in mind here is something that reorder the NarrPara and ZProof para accordingly. That is, linearly search
the AST ZSect list of paragraphs and push them all to the end of the last NarrPara or last Z-formal para in FIFO order.
This way, it becomes easy to "clean-up" the spec from proof scripts, and, at the same time, allow for as less reproof as possible.

PS:
we are still looking into proof databases (e,g., like ml pre-compiled files , say).