[octo_t]

I love type theory, but I think a language like Sage[1] is probably the most interesting way forward.

[1] - http://sage.soe.ucsc.edu/

[StefanKarpinski]

That's a somewhat unfortunate name to choose for a new language given the existence of this well-established system:

http://www.sagemath.org/

[sfvisser]

Why the 'but'? There seems to be quite some type theory involved in Sage.

[ufo]

I really like the idea behind Sage but I found it kind of funny that in their test cases all the ".out" files are empty because none of the programs actually do any IO. No hello-world for you :P

[tel]

How do you feel about dependently typed systems?

[ufo]

Sage has dependent types so he probably likes them.

[tel]

Ah, I misread the intro blurb.