> I think dependent types are the winner for next-generation languages. Anything that lets you codify more into the type system is more back pressure.

This is one reason I'm so bullish on Lean4 as a general programming language

It's now essentially proven that expressive, strong type systems like those of Rust present an advantage for LLM assisted coding

Lean's type system, in which types are first class, fully programmable objects takes it so much further. Particularly when it comes to embracing dependant types