3 ms·
> Hard to inspect but very possible test. Probably, but is testing to the necessary level of correctness more or less effort than writing the code ourselves?
by rco8786 4y ago
> Hard to inspect but very possible test.
Probably, but is testing to the necessary level of correctness more or less effort than writing the code ourselves?
- hinkley 4y agoLanguages with very high degrees of static analysis are basically making you write the tests in the code. We have people who think they can keep extending that until there's barely any code, but they haven't been proven right or wrong yet.
- layer8 4y agoStatic analysis creates proofs, which is fundamentally different from tests. Merely testing AI output will always be inferior on principle than proving code to be correct. One would have expected AI to be better than humans at proving code correct (instead of just testing it for certain inputs), but LLMs currently fall short of that.
- hinkley 4y agoWhat I'm saying is that if you have the proof, someone will write an AI to pass it. There's still a lot of very, very sophisticated work that goes into locking down requirements that tightly.
- layer8 4y ago> if you have the proof, someone will write an AI to pass it. That doesn’t make any sense. What passes the proof is the program code. You have the code, and then you construct a formal proof that the code is correct, similar to how a mathematician proves that some theorem is correct. The code is a prerequisite for the proof. When you can construct a proof for the code, you’re done. This proof-construction process is what AIs currently aren’t good at, because it requires logical precision, and probability isn’t sufficient. They can generate code, but they can’t construct the formal proof that the code is correct (and it often isn’t). > There's still a lot of very, very sophisticated work that goes into locking down requirements that tightly. What’s true is that you need to know what you want to prove about the code, and that isn’t always easy.