Ian Lynagh <[email protected]> writes: > 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.
[sorry for going into coq-specifics] I don't want to stop your enthusiasm too soon, but I don't think C-zar can do that. Sure, C-zar makes for more readable proofs, but they are not easier to write. It also seems that (at least in the current version of Coq), C-zar proofs do not give the full power of dependent induction, which we're going to critically need. In the end of the day, you're still using the same tactics, just writing their invocation differently, so the critical part is understanding a/ Coq's formal setting (CiC) b/ the behaviour of the various tactics. This makes me think we should not be relying on C-zar too much. Not that writing proofs in C-zar is bad, it just won't change the situation too much. On the good news front, I think I see an elegant way to axiomatise names and patch universes in coq, so most of the infrastructure for proving the algorithms should soon be ready. Finally an idea: how about making darcs-user the default destination for patches against camp and the camp paper. This would not change the signal to noise ratio here in a perceptible way, but it would convey the message that the theory and the implementation are going forward. Florent _______________________________________________ darcs-users mailing list [email protected] http://lists.osuosl.org/mailman/listinfo/darcs-users
