▲ | Buttons840 4 days ago | |
If LLMs get a little better at writing code, we might want to use really powerful type systems and effect systems to limit what they can do and ensure it is correct. For instance, dependent types allow us to say something like "this function will return a sorted list", or even "this function will return a valid Sudoku solution", and these things will be checked at compile time--again, at compile time. Combine this with an effect system and we can suddenly say things like "this function will return a valid Sudoku solution, and it will not access the network or filesystem", and then you let the LLM run wild. You don't even have to review the LLM output, if it produces code that compiles, you know it works, and you know it doesn't access the network or filesystem. Of course, if LLMs get a lot better, they can probably just do all this in Python just as well, but if they only get a little better, then we might want to build better deterministic systems around the unreliable LLMs to make them reliable. | ||
▲ | gylterud 4 days ago | parent [-] | |
The day when LLMs generate useful code with dependent types! That would be awesome! |