|
|
|
|
|
by raphlinus
186 days ago
|
|
There's a straightforward answer to the "why not" question: because it will result in codebases with the same kind of memory unsafety and vulnerability as existing C code. If an LLM is in fact capable of generating code free of memory safety errors, then it's certainly also capable of writing the Rust types that guarantee this and are checkable. We could go even further and have automated generation of proofs, either in C using tools similar to CompCert, or perhaps something like ATS2. The reason we don't do these at scale is that they're tedious and verbose, and that's presumably something AI can solve. Similar points were also made in Martin Kleppmann's recent blog post [1]. [1]: https://martin.kleppmann.com/2025/12/08/ai-formal-verificati... |
|