Lambda the Ultimate

The flip side is that if you will be doing honest-to-goodness dependently-typed programming, Agda and Epigram are the only practical options. If you are just writing simply-typed programs and proving theorems about them, then Coq may be more convenient. But you never know when you will start wanting to write programs.... ;-)

Okay maybe that's a little glib, but I do find Agda to be a very pleasant environment for dependent programming---I haven't used Epigram, but I believe it has many similar features. Both are in active development. In terms of programming, the big advantage of Agda/Epigram over Coq is that they have proper support for dependent pattern-matching. That is, you write dependently-typed functions using pattern-matching, more or less as you would write their simply-typed cousins in ML/Haskell, and a coverage checker verifies (using the dependent types) that no cases are missing. Additionally, Agda doesn't force you into a particular form of induction---a separate termination checker verifies (or attempts to verify) that function definitions are well-founded (and complains otherwise, but grudgingly accepts the definition). In Coq, writing dependent functions explicitly is currently much more unpleasant, although there's no fundamental reason why it has to continue to be, and Matthieur Sozeau's work has addressed some of this.

For good examples of the neat things you can program in Agda, you can try reading Nicolas Oury and Wouter Swierstra's paper The Power of Pi from ICFP 08, or some of the other papers using Agda.

Thanks guys, your replies have helped me think about what I need. Such theorems that I do need to prove will indeed fall out from the types, so using Coq is probably overkill. A convenient environment for programming is more important at this stage, and I will give more serious attention to Agda & Epigram.

There are design patterns for dependently-typed programming in Coq. They may take some time to learn, but you are set, within a constant factor, after that point.

In contrast, serious theorem-proving in Epigram or Agda is always going to be asymptotically more programmer-time expensive than it would be in Coq, no matter what the programmer learns first. The only way out of this would be to add a tactic language to one of these systems, IMO.

> In contrast, serious theorem-proving in Epigram or Agda is always going to be asymptotically more programmer-time expensive than it would be in Coq, no matter what the programmer learns first. The only way out of this would be to add a tactic language to one of these systems, IMO.

That's a very strong statement. What sort of theorem-proving tasks do you have in mind that would necessarily require a tactic language to be practical, and what features of the tactic language are required?

I'll save Adam a couple of minutes by pointing to his Certified Programming With Dependent Types. If you follow the links to the draft of his textbook, and then to the Introduction, you find:

Why Not a Different Dependently-Typed Language?

The logic and programming language behind Coq belongs to a type-theory ecosystem with a good number of other thriving members. Agda and Epigram are the most developed tools among the alternatives to Coq, and there are others that are earlier in their lifecycles. All of the languages in this family feel sort of like different historical offshoots of Latin. The hardest conceptual epiphanies are, for the most part, portable among all the languages. Given this, why choose Coq for certified programming?

I think the answer is simple. None of the competition has well-developed systems for tactic-based theorem proving. Agda and Epigram are designed and marketed more as programming languages than proof assistants. Dependent types are great, because they often help you prove deep theorems without doing anything that feels like proving. Nonetheless, almost any interesting certified programming project will benefit from some activity that deserves to be called proving, and many interesting projects absolutely require semi-automated proving, if the sanity of the programmer is to be safeguarded. Informally, proving is unavoidable when any correctness proof for a program has a structure that does not mirror the structure of the program itself. An example is a compiler correctness proof, which probably proceeds by induction on program execution traces, which have no simple relationship with the structure of the compiler or the structure of the programs it compiles. In building such proofs, a mature system for scripted proof automation is invaluable.

On the other hand, Agda, Epigram, and similar tools have less implementation baggage associated with them, and so they tend to be the default first homes of innovations in practical type theory. Some significant kinds of dependently-typed programs are much easier to write in Agda and Epigram than in Coq. The former tools may very well be superior choices for projects that do not involve any "proving." Anecdotally, I have gotten the impression that manual proving is orders of magnitudes more costly then manual coping with Coq's lack of programming bells and whistles. In this book, I will devote significant time to patterns for programming with dependent types in Coq as it is today, and I will also try to mention related innovations in Agda and Epigram. We can hope that the type theory community is tending towards convergence on the right set of features for practical programming with dependent types, and that we will eventually have a single tool embodying those features.

Thanks for the link, Adam's draft book looks most interesting.

I didn't say anything about "tasks that require a tactic language to be practical." It's about whether there is a good supply of real-world projects that involves non-trivial theorem proving where it would make sense to choose a proof assistant without a programmable tactic system. I think there isn't. The developer would waste too much of his time writing proofs manually.

...that most tactics can be embedded into a programming language via large eliminations. The Nuprl people were doing this systematically almost 20 years ago -- see Allen et al's LICS 1990 paper "The Semantics of Reflected Proof". Obviously, there's a great deal of engineering effort in taking a basic type theory up to the level of a system as mature as Coq, but I don't see any fundamental theoretical obstacles. Do you have anything specific in mind?

And most programs could be written in assembly language, but it's widely recognized that that isn't usually the right tool for the job. It's clear to me at this point that dynamic typing is the only way to go for a tactic language. I'm not interested in "fundamental theoretical obstacles" so much as cost-benefit trade-offs in real engineering. We can argue about this abstractly ad infinitum with no conclusion; I would need to see a real, production-quality proof assistant with certified reflective tactics to believe that it's possible.

I use dynamic type errors as control operators all the time in my Coq proof scripts, and it's amazingly useful.

There is actually some deep reason why dependent pattern-matching is not allowed currently in Coq. Cristina Cornes had implemented everything needed in Coq 10 years ago, but was reluctant to add this to the system (and presumably her advisor Gerard Huet too) because it deeply relies on Streicher's axiom K which is not derivable in the Constructions. I'm currently reviving this work using the techniques of Goguen, McBride and McKinna in Coq, still relying on K. The point is that this axiom will probably be internalized sooner or later, alone or as part of an implementation of proof-irrelevance. But the question of this extension is still subject to debate inside the community: witness this thread on the Agda wiki where Coquand points out some of the problems with K.

thanks for the background and updates.

The flip side is that if you will be doing honest-to-goodness dependently-typed programming, Agda and Epigram are the only practical options.

Is ATS not a practical option (and if not why not)?

I was being hyperbolic, because I thought Adam's statement (which I bowdlerized) was too dismissive of Agda/Epigram. Certainly, ATS can be a good framework for certain kinds of programming/theorem proving -- it depends what programs you're trying to write/what theorems you're trying to prove.

I was being hyperbolic

For those of us how don't know much about dependently typed systems, that just isn't helpful.