[mej10]

This looks awesome! I will be interested to see how well you can make the features fit together. I have been really interested in languages that give you tools for reasoning at multiple levels of abstraction.

Have you tried seeing how a full dependent type system could be used in your design?

[daivd]

I plan to sneak in something similar with a capable type system and contracts for stuff that you can't express in the types. That way you could "one day" use a solver like Z3 and start proving or disproving some of the tractable contracts, without having to even change the programs. A bit like LiquidHaskell.

Not exactly dependent types, but practical, I think.