Comment by Buttons840
6 months ago
Yes, we need to build deterministic systems that the AI can work within.
I wonder if we'll ever use AI to write code in dependently typed languages. Dependent types can check almost anything at compile time; they can check that a function returns only sorted data, they can check that the submit_order function only submits valid orders--again, they can check this at compile time.
So, we could express a variety of high level constraints and let the AI go wild, and as long as the resulting code compiled, we would know it was correct, because the type system confirms it.
If we also include an effect system, then the type system could say things like "this function will return a valid Sudoku puzzle solution, and it will not access the network or filesystem", and then, if it compiles, we know the those conditions will hold at runtime.
That’s the dream with dependent type systems, but from my very limited exposure to them, it seems like it’d be very difficult to encode complex constraints like all of your company’s business logic in this way.
Not saying it can’t be done, but I think it’s a bit telling that no such language has ever caught on.
Unit testing can also be used to verify such constraints and is much simpler. It obviously doesn’t guarantee correct behavior like a proof, but if the tests are comprehensive, it can do a great job.
> we need to build deterministic systems that the AI can work within
That's the ordering system the AI crashed by trying to order ten thousand piña coladas or whatnot.
> I wonder if we'll ever use AI to write code in dependently typed languages
Yeah, I write code in Lean with AI pretty frequently lately