Dependent types is one possible direction. Not sure when a language with dependent types will arise which will be useful for making real programs.

Agda is the most mature dependently typed programming languae (having been around since the 90s – it is basically Haskell on steroids), but has a more proof-assistant flavor than an actual programming language flavor. Opus & Fable write Agda quite well, so LLMs can understand dependent types.

Anything with ranged numeric types. Like everyone's favorite functional programming language, Ada.

Lean 4, Idris 2.

Perhaps coq/agda/idris/etc.