The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 14/05/2020 17:04, Xavier Leroy wrote:
> The problem I see here is that most efficient data structures I can
> think of are not freely generated by constructors, but have richer
> structural invariants that need to be maintained using predicates and
> proof terms.  (For example, Frédéric Besson mentioned Patricia trees.  I
> played with them in Coq a while ago and they have plenty of structural
> invariants.)  So, this phenomenon of proof terms growing linearly with
> the number of operations performed seems hard to avoid.
> 
> It could be that there is a fundamental tension between 1) having
> efficient data structures, and 2) building valid proof terms.  That
> would make me sad.

If your well-formedness predicate is decidable, you can always replace
it by a proof that the computational boolean version is equal to true.
Now you're trading proof size for computation time, which may be worse,
or not, if you proofs are similarly efficient.

So is life in the world of proofs-as-programs, and only people
brainwashed by realizability believe that substanceless proofs float
around in a space of ethereal truth.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature