- It isn't open source right now. I think that's best while the language is still developing, but I plan on opening it up once things have settled down. I don't want to have legacy code before I've even started :P
- No, that aspect is fairly tangential. Since my language is heavily based on the lambda calculus, I already have pretty good basis for nice type properties. I don't have a formal semantics right now, so it will be a while before any such proof would even be possible.
- Both hopefully! I totally understand this dilemma. As lots of people here have pointed out, there is a lot of work to be done on the implementation, but the theoretical aspects of the language have to be a higher priority for the next couple months. It's stressful!
I wish you the best on your project! It sounds really ambitious / useful. I imagine such an analysis could help generate much faster code too.