|
|
|
|
|
|
by krisoft
496 days ago
|
|
|
> I want a chatbot that can automatically magic up proofs that all my code is correct for instance. How could the AI know what you wanted to program? If it was trained only with self play it won’t understand the language where you describe the purpose of the code because it only speaks its own idiosyncratic language. (At best.) And if it doesn’t know what you wanted to do then all it can prove is that the program does what the program does. |
|
|
The tooling surrounding it might want to prove that "this main function never invokes undefined behavior", or something more local like "for all possible inputs to the public interface to this module, no undefined behavior is invoked".
Or you might want to specify constraints by hand. For examples, you might do that by writing normal tests except you can use magical variables that take on any value [1], or you might do that by annotating functions with contracts that they obey [2]. Or at a simpler level you might just annotate functions that should never panic.
Ultimately once you can prove things about your code, it's a tool in the toolbox for querying how your code works. You can use that to write correct code from the start, or to debug incorrect code, or various other things. The problem is that right now the state of the art (non-ai) can't reason about very complex code without a lot of human help - making it a fairly impractical tool. I think AI might mange to fix that.
[1] This is how kani works in rust, here's an example: https://github.com/model-checking/verify-rust-std/pull/112/f...
[2] Creusot takes this route, here's an example https://github.com/sarsko/CreuSAT/blob/master/CreuSAT/src/so...