[throwaway17_17]

I think you share a lot of my interests on the theory side of things. I also share your belief that those areas probably can allow for the development of the core of systems level programming language. Of course, I tend to find that graded, or the more general contextual modal type theory subsumes multi-staged, two level and grade modal theories. I also think a broad spectrum dependently typed language (with modal enforcement of computational irrelevance) can take care of dependent modules.

I think you are also spot on about Rust having a strangeness budget and that could be responsible for the syntactic state of the language as it exists today. I have a much higher tolerance for non-conventional syntax so almost all of my type theory implementation and PL work has been outside the normal syntactic bounds for the last 2 years. I doubt I ever produce a language that is public, let alone a language that is used by any portion of the software engineering field. But my belief is that this arena is fertile ground for a more fundamental core, like you mentioned.

As an aside, I happened to stumble upon Andras’ video presentations on YouTube on Saturday and flagged them to watch and bookmarked the repo for them earlier today. So bravo on linking what look to be really nice resources for this area of work.