This is all quite impressive, but I have a word of caution. I was involved, decades ago, in a project with research-grade programming languages and type systems (https://research.ibm.com/publications/the-type-inference-and-coercion-facilities-in-the-scratchpad-ii-interpreter). The bitter lessons that I learned:
- There are very few people who can master the abstractions and use them effectively (roughly, the top 1% of academic applied-mathematicians and computer-scientists)
- The queue of edge cases needing clarification seemed to never end. This problem was hidden by the fact that only one implementation existed, and so became the definition of behaviour. A misty landscape.
- Language experts got bored (presumably) with the implementation chores and moved to other projects, leaving the implementation without expert support.
- Early adopters of the fancy features found it difficult to translate their insights to other environments and consequently their influence among their peers waned.
- Despite the promise, big breakthroughs were achieved by other attempts, some being heroic one-man efforts with a far more pedestrian programming language.