[darcs-devel] (un)safety of unsafeCompare

Ben Franksen ben.franksen at online.de
Sat Jul 6 19:43:40 UTC 2019


Am 06.07.19 um 18:23 schrieb Ganesh Sittampalam:
> I think what you say about "better make sure that all the other
> operations are consistent with that definition" is exactly what I am
> thinking of when I say "proof obligation".

Okay, fine.

> If you do violate that proof obligation, so that supposedly equal
> patches don't produce the same result when applied, then you end up
> being able to do the exact equivalent of 'apply (unsafeCoerceP x)'.

Hm, yes. Good point.

> I don't think we disagree about what code would be correct and what
> wouldn't, so the question is just how to communicate that to others. I
> don't feel too strongly about exactly how we do that.

I will try to think of a way to make this point clear in the
documentation. Perhaps referring to patch application is a good way to
do that. If only 'apply' didn't have this meaningless type...

Cheers
Ben



More information about the darcs-devel mailing list