[darcs-users] marketing, darcs-2 bugs and a tiny bit about darcs 3

[Florent Becker]

> 
> 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