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

Ian Lynagh igloo at earth.li
Tue Mar 17 14:12:52 UTC 2009


On Tue, Mar 17, 2009 at 10:40:01AM +0000, Florent Becker wrote:
> 
> > 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.

I've also been looking at whether we can use the coq's new C-zar
language to allow us non-experts to write proofs more easily. However,
currently there are a couple of things I don't know how to do in C-zar,
so I'm not currently able to make any progress there. Hopefully I'll get
some answers soon, and then should have a better idea on how to move
forwards.


Thanks
Ian



More information about the darcs-users mailing list