| ▲ | seanmcdirmid 2 days ago | |||||||||||||||||||||||||
As long as your program is large and multi-threaded (most programs that matter commercially), it is not very analyzable or repeatable. You replace those qualities with QA and tests, the same is true with prompting. | ||||||||||||||||||||||||||
| ▲ | Rapzid a day ago | parent | next [-] | |||||||||||||||||||||||||
Sounds like it's time for your LLM daddy to have the Coq talk with you.. | ||||||||||||||||||||||||||
| ▲ | friendzis 2 days ago | parent | prev [-] | |||||||||||||||||||||||||
Eve if "write code -> run QA -> analyze failures -> rewrite code" is cheaper for most commercial software than thorough upfront formal verification, it works precisely because the programs are analyzable. When the code spit out by an LLM does not pass QA one can merely add "pls fix teh program, bro, pls no mistakes this time, bro, kthxbye", cross their fingers and hope for the best, because in the end it is impossible -- fundamentally -- to determine which part of the prompt produced offending code. While it is indeed an interesting observation that the latter approaches commercial viability in certain areas there is still somewhere between zero and infinitesimal overlap between prompting and engineering. | ||||||||||||||||||||||||||
| ||||||||||||||||||||||||||