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

[ivan-gandhi.livejournal.com]

It is pure intuitionistic logic. Pretty readable, too. I saw it first time.