4 ms·
> I can tell when it spits out a snippet of code that is correct, and when it's wrong. Hah, sure. Okay. How? You just read it and think really hard? Bertrand
by agentultra 3y ago
> I can tell when it spits out a snippet of code that is correct, and when it's wrong.
Hah, sure. Okay. How? You just read it and think really hard?
Bertrand Meyer, the inventor of Eiffel, who rants about software correctness all the time -- didn't notice an error in a 1-line expression in Eiffel that was generated by ChatGPT [0].
If you spend a little time formalizing correctness in a theorem prover or model checker you may not be so confident that you can read a snippet of code and know that it's correct. In order to know that you have to be able to write the specification precisely. Natural language is not precise enough.
Update: You may be able to write the specification precisely either by modelling the system and checking the model or writing a theorem and proving it... but so far LLM's cannot reason on that level.
[0] https://buttondown.email/hillelwayne/archive/programming-ais-worry-me/ https://buttondown.email/hillelwayne/archive/programming-ais...