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...

▲

nu11ptr 17 hours ago | parent | next [-]

It is also equally odd to me that people want to cling so hard to C, when something like Rust (and other modern languages for that matter), have so much nicer eco systems, memory safety aside. I mean C doesn't even have a builtin hashtable or vector, let alone pattern matching, traits and sum types. I get this is about AI and vibe coding, but we aren't at a point yet where zero human interaction is reasonable, so every code base should assume some level of hybrid human/AI involvement. Why people want so badly to start a new code base in C is beyond me (and yes, I've written a lot of C in my time, and I don't hate it, but it didn't age well in expressiveness).

	▲	benjiro 14 hours ago \| parent [-]
		> It is also equally odd to me that people want to cling so hard to C, when something like Rust (and other modern languages for that matter), have so much nicer eco systems, memory safety aside. Simplicity? I learned Rust years ago (when it was still pre release), and when i now look at a lot of codebases, i can barely get a sense what is going on, with all the new stuff that got introduced. Its like looking at something familiar and different at the same time. I do not feel the same when i see Go code, as so little has changed / got added to it. The biggest thing is probably generics and that is so rarely used. For me, this is, what i think, appeals for C programmers. The fact that the language does not evolve and has been static. If we compare this to C++, that has become a mess over time, and i know i am getting downvoted for this, Rust feels like its going way too much in the Rust++ route. Like everybody and their dog wants something added, to make Rust do more things, but at the same moment, it feels like its repeating the C++ history. I have seen the same issue with other languages that started simple, and then becomes monsters of feature sets. D comes to mind. So when you see the codebase between developers, the different styles because of the use of different feature sets, creates this disconnect and makes it harder for people to read other code. While with C, because of the language limits, your more often down a rather easier way to read the same code. If that makes sense?

▲

doug_durham 16 hours ago | parent | prev [-]

Proofs of what? "This new feature should make the 18 to 21 year old demographic happy by aligning with popular cultural norms". This would be difficult to formalize as a proof.

	▲	raphlinus 16 hours ago \| parent \| next [-]
		Memory safety in particular, actually UB in general (got to watch out for integer overflows, among other things). But one could prove arbitrary properties, including lack of panics (would have been helpful for a recent Cloudflare outage), etc. In order to prove lack of UB, you have to be able to reason about other things. For example, to safely call qsort, you have to prove that the comparison is a total order. That's not easy, especially if comparing larger and more complicated structures with pointers. And of course, proving the lack of pointer aliasing in C is extremely difficult, even more so if pointer arithmetic is employed.
	▲	IshKebab 15 hours ago \| parent \| prev [-]
		In this context it's proofs of properties about the program you're writing. A classic one is that any lossless compression algorithm should satisfy decompress(compress(x)) == x for any x.