Recently, I have been interested in programming languages with dependent data types, mostly because they seem to be the natural end point of type system evolution. (Perhaps "end point" is the wrong term; "next step" may be better.) Unfortunately, most of the dependently typed languages I have seen are unappealing for various reasons.
- Epigram seems neat, but the last time I looked at it I seem to recall it only worked within its own IDE. Not a terrible failing, but still.... And version 2 is not out yet.
- Agda also seems neat, but for some reason I am having a hard time getting enthusiastic about it.
- Coq is neat (there may be a trend here), but as a programming language? Certainly, it is the best computer game I have played in ages, but one issue I have is that I find Coq proofs almost unreadable. It does get lots of extra points for Coq'Art, a truly excellent book.
- Many of the others that I have heard about are not actively developed.
Damn, I'm inadequate.
[Edit: Yah, and I can't even remember to tag my posts.]