Dependent types is one possible direction. Not sure when a language with dependent types will arise which will be useful for making real programs.
replyAgda 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.
replyThis issue raises SIGFPE. Ada would raise Constraint_error, which is easier to catch than a signal, but still occurs at runtime.
replyYou need range proofs to be 100% safe, and then you can as well use the regular type because invalid values will not occur.
Or Liquid Haskell.
replyLean 4, Idris 2.
replyPerhaps coq/agda/idris/etc.
reply