Comment by ben_w

> 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.