4 ms·

Imagine if the AI can provide both a program and a machine-verifiable proof of correctness though. Then all you have to manually verify is that the proof proves

by im3w1l 4y ago

Imagine if the AI can provide both a program and a machine-verifiable proof of correctness though. Then all you have to manually verify is that the proof proves the right thing.

acuozzo 4y ago
How will the AI overcome the halting problem?
- pulvinar 4y ago
  Well humans haven't overcome it, and we muddle through. Same with AI, it seems.
- torginus 4y ago
  Easy - it will come up with a solution too complicated for mere humans to understand, at which point everyone will assume it is correct.
- TheCoelacanth 4y ago
  The same way that humans do. By redefining "doesn't halt" as "didn't halt before my patience ran out".
- karmakaze 4y ago
  You can't in general determine if an arbitrary program will halt. I believe it is however, possible to construct a program that does provably halt. I have no idea if you can write most useful programs that way though.
  - im3w1l 4y ago
    Almost all programs that people write are written so that they provably halt (or provably don't halt - as continuing forever is sometimes the desired behavior). How do we do that? By using known-halting parts, and composing them in known-halting ways. How did we find those parts in the first place, well computer science.. But boiling that down to a codified process, that's where it gets murkier. I think we don't really know exactly how human ingenuity discovers new useful halting parts in the face of the halting problem.
goto11 4y ago
So the only thing a developer have to deliver is an unambiguous specification of what the program is supposed to do!
- bguebert 4y ago
  If I could get unambiguous specifications, then my job might actually be in trouble. It would cut my workload down considerably.
  - goto11 4y ago
    I was half joking, because software development is largely the process of developing an unambiguous specification - just in the form of executable code.
- TheCoelacanth 4y ago
  That sounds hard to do in a natural language. Maybe they could deliver the unambiguous specification in a formal language designed specifically for the purpose of specifying what programs are supposed to do.
- euroderf 4y ago
  A premium on the ability to express requirements clearly and logically, on the fly rather than as part of a cycle of paper-pushing.

by im3w1l 4y ago

Imagine if the AI can provide both a program and a machine-verifiable proof of correctness though. Then all you have to manually verify is that the proof proves the right thing.

acuozzo 4y ago

How will the AI overcome the halting problem?

pulvinar 4y ago
Well humans haven't overcome it, and we muddle through. Same with AI, it seems.
torginus 4y ago
Easy - it will come up with a solution too complicated for mere humans to understand, at which point everyone will assume it is correct.
TheCoelacanth 4y ago
The same way that humans do. By redefining "doesn't halt" as "didn't halt before my patience ran out".
karmakaze 4y ago
You can't in general determine if an arbitrary program will halt. I believe it is however, possible to construct a program that does provably halt. I have no idea if you can write most useful programs that way though.
- im3w1l 4y ago
  Almost all programs that people write are written so that they provably halt (or provably don't halt - as continuing forever is sometimes the desired behavior). How do we do that? By using known-halting parts, and composing them in known-halting ways. How did we find those parts in the first place, well computer science.. But boiling that down to a codified process, that's where it gets murkier. I think we don't really know exactly how human ingenuity discovers new useful halting parts in the face of the halting problem.

goto11 4y ago

So the only thing a developer have to deliver is an unambiguous specification of what the program is supposed to do!

bguebert 4y ago
If I could get unambiguous specifications, then my job might actually be in trouble. It would cut my workload down considerably.
- goto11 4y ago
  I was half joking, because software development is largely the process of developing an unambiguous specification - just in the form of executable code.
TheCoelacanth 4y ago
That sounds hard to do in a natural language. Maybe they could deliver the unambiguous specification in a formal language designed specifically for the purpose of specifying what programs are supposed to do.
euroderf 4y ago
A premium on the ability to express requirements clearly and logically, on the fly rather than as part of a cycle of paper-pushing.