> > But darcs-2 is not perfect. Bad things can happen, rarely, perhaps; but > the possibility is still there. The darcs-2 format is still a net > improvement over the darcs-1 format in my opinion, but over the long run > we will need to work on darcs-3. The good news is that Ian has gotten a > head start with his work on camp; I hear proving things with Coq is > involved! > I'm not sure if "involved" is the right term: I started proving Ian's theory in coq, but i'm nowhere near expert enough in coq. At some point, Ian's formalisation may be realized in coq, but proving darcs3/camp's code in coq is way out of our reach for the moment. Still, if you are interested in this effort, the coq code lives in the same repo as the camp paper, http://code.haskell.org/camp/devel/paper. I'd be very glad to have someone else who knows coq and darcs look at it.
Florent _______________________________________________ darcs-users mailing list [email protected] http://lists.osuosl.org/mailman/listinfo/darcs-users
