Dependant languages let you express almost anything in the type system. "The array I receive will contain only valid Sudoku solutions", you can express that and

Dependant languages let you express almost anything in the type system. "The array I receive will contain only valid Sudoku solutions", you can express that and the compiler can confirm it's true at compile time. This is very powerful but requires writing proofs to help the compiler. I wonder if LLMs could help here? It's a burden to write the proofs, but if LLMs become good enough and flexible enough, the dependant type system might serve as a formal layer on top of a LLM, while the LLM fills in the proofs for us. A dependant type system could serve as the "world" an AI lives and grows in. Currently LLMs mimic our words without a reality to push back. LLMs can't be wrong, they try to mimic, but they have no hard limitations, whatever word they spit out has only soft rewards or punishments. A type system could be the reality an AI lives and learns in, with a hard ground it can fall on, hard walls it cannot pass, and other hard limitations it can explore in.