Comment by ben_w
16 hours ago
> How can it be proven correct if it's not deterministic?
Depends on domain, but basically all the same lessons we have for software written the old way by humans.
Which, ah, admittedly isn't great.
> Isn't this the halting problem?
No.
1. The halting problem applies specifically to deterministic systems; there may be a non-deterministic equivalent, but not enough people cared before AI got good.
2. For practical purposes, it's fine to reject things that take too much effort to prove correct.
3. "Proven correct" is different from "proven to halt eventually". I guess Gödel's incompleteness theorems would be a partial fit, but even then the goal here is to reject anything you can't prove, rather than the much harder (impossible) challenge of proving the validity of all possible statements it might come up with.
> 1. The halting problem applies specifically to deterministic systems; there may be a non-deterministic equivalent, but not enough people cared before AI got good.
Making your Turing machine non-deterministic doesn't add any power to it in the sense that the halting problem cares about.
> 2. For practical purposes, it's fine to reject things that take too much effort to prove correct.
Even more so: in practice you write software and proof together. Forget about being able to prove anything about arbitrary software that was written with no proof in mind.
> 3. "Proven correct" is different from "proven to halt eventually". I guess Gödel's incompleteness theorems would be a partial fit, but even then the goal here is to reject anything you can't prove, rather than the much harder (impossible) challenge of proving the validity of all possible statements it might come up with.
Proven correct is a much stronger statement than proven to halt eventually. The form usually has to include the latter.
But yes, as said before, we only prove software that's specifically co-written to be easy to prove.