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

Florent Becker florent.becker at ens-lyon.org
Wed Mar 18 08:01:19 UTC 2009


Ian Lynagh <igloo at earth.li> 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



More information about the darcs-users mailing list