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

http://www.sagemath.org/

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

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

How do you feel about dependently typed systems?

Sage has dependent types so he probably likes them.

Ah, I misread the intro blurb.