Dependent types & ATS language

[bearophile]

I am learning something about the Dependent Types, it's a type of type system. Some of you may be interested, so here are few notes.

There's a Wikipedia page about Dependent types, but it doesn't explain enough for me, so no URL here. 

As it often happens, those someone has put part of those computer science ideas inside a programming language, this is named ATS. If programmed well it is about as fast as C, it allows some theorem proving, it may be used to write Linux device drivers, and it has Dependent types (and linear types):
http://en.wikipedia.org/wiki/ATS_%28programming_language%29

I have started to understand dependent types and what's good in them after reading this page, that while surely showing not much about ATS, shows some ideas that I didn't know:
http://www.bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.html

There are other languages for theorem proving like Coq, but they look even harder to use than ATS.

Using ATS its author was able to create a (not efficient, list-based) QuickSort that guarantees that it always returns a list that is a sorted permutation of its input, this is not an easy feat at all:
http://www.ats-lang.org/EXAMPLE/MISC/listquicksort_dats.html

But what has sold me on the dependent types is this, it implements red-black trees, this ATS program implements the insertion and balancing, plus correctness proof, so probably this is correct code:
http://www.bluishcoder.co.nz/ats/dt8.dats

If you have tried to implement red-black trees in C you know that you produce a four times longer program that often at the first implementation contains some hard to find bugs.

ATS is not a general purpose language, it's for low-level code that needs to be a bit safer.

Bye,
bearophile