Re:Software 2.0
by layer8 on Tuesday February 21, 2023 @02:51PM
(#34886091)
> 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.
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.