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 _______________________________________________ darcs-users mailing list [email protected] http://lists.osuosl.org/mailman/listinfo/darcs-users
