Record time speedrun from "I'm putting my foot down in favor of AI" to "at least 1/3 of patches are flat out wrong or harmful", eh?
post
Nice, I can get behind that policy. LLMs can be useful but only if you assume the output is wrong until proven correct. Using it to find potential threads to pull at makes sense to me but not blindly trusting everything it points out
Actually proving that C code is correct is not easy.
Having a human developer manually write code that is less harmful/wrong, and doesn't require proof, is probably easier.
Except a good programmer will have proof, in the form of at minimum manual tests that exercise the exact issue. A good programmer will have automated tests that clearly assert the behavior in question.
It genuinely boggles my mind when people whine about having to prove what the AI said... THEY SHOULD'VE BEEN DOING THAT THE WHOLE FUCKING TIME in their entire career!
We're talking about different kind of proofs.
Proving a program is correct requires a formal specification and a formal verification with mathematics and/or formal methods. ie proving the behavior and result perfectly match specification for all possible inputs.
A test only proves that a program 1) returns the expected output for a specific input, or limited set of inputs, and 2) appears to behave correctly, ie there may be undefined behaviour but they don't cause an immediate crash.
lol no. Absolutely no. In any way. Ever. A bug either works or it doesn't. The fact you think I'm talking about something else means you are already cooked, utterly and completely. Sad.
No one proves their code is correct except in extremely niche cases. No idea what you're talking about.
Test based development is not something you see much in the world of C
AI is a tool. And with every tool, there is a right way to use it, and a wrong way to use it.
all 19 comments