[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