top | item 32821074

(no title)

bjz_ | 3 years ago

I think it's more a reflection of how Rust evolved, and the techniques and approaches known and understood at the time and the strangeness budget they were (understandably) willing to take on at the time as opposed to something inherent. And also sometimes having separate, complicated features for similar things (as opposed to simple, generalised features that compose powerfully) can be useful pedagogically as well.

At any rate, this is something I'm personally interested in based on my experience working with Rust over the last decade, and so that's why it appears so high up on my list. Often you really do want sub-languages for different purposes, but managing how they interact and work together, what is the same and what is different, and how that impacts usability is interesting (and difficult) part. I feel like it should be possible to do this, but it's going to take some work and there's still lots of unknowns.

In technical terms, I'm interested in dependently typed module systems, multistage programming[1], graded modal type theory[2], elaborator reflection, and two level type theory[3]. These all sound pretty intimidating, but you can actually see glimmers of some of this stuff in how Zig handles type parameters and modules, for example, something that most programmers really like the first time they see it!

I do feel like there is the core of a simple, flexible, powerful systems language out there... but finding it, and making it approachable while maintaining a solid footing in the theory and being sensitive to the practical demands of systems programming is a nontrivial task, and many people will be understandably skeptical that this is even a good direction to pursue. Thankfully the barrier to entry for programming language designers to implementing languages in this style has reduced significantly in just the last number of years[4], so I have hope that we might see some interesting stuff in the coming decade or so. In the meantime we have Rust as well, which is still an excellent language. I'm just one of those people who's never content with the status quo, always wishing we can push the state of the art further. This is why I got excited by Rust in the first place! :)

[1]: https://github.com/metaocaml/metaocaml-bibliography

[2]: https://granule-project.github.io/

[3]: https://github.com/AndrasKovacs/staged

[4]: https://github.com/AndrasKovacs/elaboration-zoo/

discuss

order

throwaway17_17|3 years ago

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.