(2) Incredibly powerful type inference system, similar to those in purely functional languages. I've been eyeing "Liquid Typing" which incorporates SMT solvers to get as close as possible to prove correctness of a program (while still being decidable and not requiring type annotations).
(3) I would love interoperability with other things (Java/Python/C), but that's a lot of work and possibly infeasible as a single human being.
But I think the first place to start is actually with the typing system.
