[darcs-users] Formal documentation

[Michael Olney]

> The key property is that any given set of patches, you get the same
> repository state no matter what order those patches are currently stored in.
> That underpins the "first-class cherry-picking" and "no fresh commit for
> merges" that darcs has and other VCS systems don't.

I guess I'm not clear as to who these proofs are supposed to convince,
and of what. Without a more specific interpretation of the theory or
more properties it doesn't seem possible to prove, for example, that
I'm not going to lose any important information during the merging
process.