Agda. The language of the distant but imminent future.

[juan_gandhi]

Larry Diehl's yesterday slides

So, the language where type-dependence reaches the ultimate, where intuitionistic logic is just another way to express things. It was absolutely amazing.

Comments

[itman.livejournal.com]

It vaguely resembles APL.

[antilamer.livejournal.com]

Quite a pity that the slides don't show any reasonably complex proofs, only trivial things.

Have you looked at Coq (http://coq.inria.fr)? It's in the same direction but more complex/advanced (or complicated, if you like). They proved the 4 color theorem with it.