>>>>> "Juliusz" == Juliusz Chroboczek <[EMAIL PROTECTED]> 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.
_______________________________________________
darcs-users mailing list
[email protected]
http://www.abridgegame.org/mailman/listinfo/darcs-users
