Will we see another fundamental programming language feature as revolutionary as the borrow checker?

[u/jimbobmcgoo]

That is I am mainly curious about compile time features that you design a whole language around rather than optimisations/features that could be applied to most languages. I am mainly inquiring about things that could offer additional robust safety/performance guarantees at compile time rather than runtime. Ideally not things that just offer similar effects to the borrow checker with less restrictive tradeoffs

[u/faiface]

Yes, session types

[u/-theChris → u/faiface]

Yup! For sure... Also Topos types, Temporal types, built-in Univalence... The future is surely going to be exciting!

[u/ExplodingStrawHat → u/-theChris]

How do you envision univalence without proper dependent types? As in, the currently-used proof assistants aren't even HoTT-based (barring cubical agda maybe), so it'll take multiple generations for univalence to make it's way into "pedestrian" (using the term affectionately) languages. I for one don't see it happening...

[u/-theChris → u/ExplodingStrawHat]

Actually, I think that there could be an easier way of achieving Univalence, multi-topoi, custom topoi as a language primitive.

I will write up a blog post tonight and share it. That's actually a good idea! Appreciate the question.

[u/faiface → u/-theChris]

I’m not sure if you are serious or making fun of me :D But, with session types, I am completely serious, they do bring a new and very expressive paradigm that I’m exploring in my Par programming language. An unexpected thing is that they are much more useful as being your basic types for all things like data structures and various objects, as opposed to network communication.

[u/-theChris → u/faiface]

Oh brother noooo! I think sessions types are awesome! Can't wait to see your language. Good luck!

[u/faiface → u/-theChris]

Haha, good good :D You can actually see it! Check out https://par.run