[darcs-users] The theory of patches

[Stephen J. Turnbull]

>>>>> "Juliusz" == Juliusz Chroboczek <Juliusz.Chroboczek at pps.jussieu.fr> writes:

    Juliusz> Thus, I believe that we should refrain from adding
    Juliusz> another formalisa- tion to the manual until we have one
    Juliusz> that is powerful enough to allow a formal proof of the
    Juliusz> correctness of the Darcs model (not necessarily of the
    Juliusz> algorithms used in Darcs, mind you).

That's where we're headed.  Playing with the groupoid/category
formulation has already led to support for the conjecture that
assuming invertibility of all patches is untenable if we want a
powerful theory of patches.

Also, I don't think that kind of thing can be _proved_, as different
people will have different ideas of what is powerful enough, and what
the power is needed for.  However it's useful to have the alternative
formulation as a language for discussing this aspect of the theory.

_If_ and _when_ to put it in the manual is another question, but
that's one _we_ don't have to answer.  David will do that. :^)

-- 
School of Systems and Information Engineering http://turnbull.sk.tsukuba.ac.jp
University of Tsukuba                    Tennodai 1-1-1 Tsukuba 305-8573 JAPAN
               Ask not how you can "do" free software business;
              ask what your business can "do for" free software.