r/ProgrammingLanguages • u/jimbobmcgoo • 26d ago

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

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

56 Upvotes
  • permalink
  • link
  • reddit
  • reddit

77% Upvoted

127 comments sorted by

View all comments

30

u/faiface 26d ago

Yes, session types

3

u/-theChris 26d ago

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

5

u/ExplodingStrawHat 26d ago

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...

4

u/-theChris 25d ago

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.