Lambda the Ultimate

I'm not sure about ATS in particular, but I think it follows a similar route to DML.

I think Hongwei Xi, the main researcher behind ATS, was also behind DML, but it's my understanding that ATS was created as an alternative to Pure Type Systems, while retaining its dependent typing power. I could be wrong though, hence the request for clarification. :-)

DML only has a restricted form of dependent types, added to a conventional language.

Yes, I'm aware of this. I've seen a vague reference or two to ATS also supporting "restricted dependent types", but it was never clarified in more laymen's terms.

I also feel Ontic is important.

Indeed, I've heard a few rumblings on Ontic here and there, but it doesn't seem like much work is happening in that direction.

Then there are the various proof assistants - Coq, LEGO, etc. I don't have much experience with these.

ATS has support for combining programming with theorem proving, which is why it seems so strange that it's been discussed so little here. It seems very interesting.

I feel the strongest difference is what kind of programs you can write with which expressiveness in specifications.

• For DML it is ML with automatic proving for arithmetic expressions in types. The other allow roughly the same expressiveness in specifications.
• Epigram is powerful just as Coq and LEGO, it is a really dependently typed programming language where proof and algorithmic code are intermingled in an elegant way.
• ATS separates proving and coding a little more and proposes other paradigms than functional programming. The main difference i see between Epigram and ATS is on the objective. The first proposes a new way of programming while the second integrates all paradigms in an unifying one using dependent types and relying explicitely on the manipulation of proof objects.
• In Coq (and probably LEGO), you could write the same programs as in Epigram, except it would generally be a nightmare for a number of practical and theoretical reasons. Epigram is a programming language giving you adapted syntax and constructs to program, and a nice typing and editing system. Here tactics to prove/program are part of the language (rec, <=, case, etc...).
  On the other hand, Coq and LEGO are proof assistants, so their main focus is on proving, not on the easy manipulation of terms. That's kind of where Curry-Howard stops for them, you can write terms with simple types easily, but once you want to give a rich specification to a program you're alone. You can use the tactic language to prove arbitrarily complex goals but it's a bad idea to use them for creating programs.

Thanks for the explanation! It would seem then, that ATS may be more verbose, but still theoretically as powerful as Epigram. The "backwards-compatible" paradigms are certainly interesting though, if only to see how they're typed, and it should yield an idea of how useful they actually are.