[gurps] Failing autopilots and RVO

[Zan Lynx]

Anthony Jackson wrote:
> Onno Meyer wrote:
>> Travis replied to me:
>>> I see no reason that the proof is only for machines, it also applies
>>> to methods or procedures that involve one or more people.
>>
>> If those people follow an algorithm. Humans can decide not to
>> do that.
> 
> If you're going to provide proof, you necessarily use an algorithm. Note 
> that certain types of unsolvable problems are only unsolvable from 
> within the system being analyzed, which means an _external_ computer may 
> be able to determine whether a given program will halt when the computer 
> that the program will run on cannot. This exception also applies to a 
> human analyzing a computer program -- because he's external, he can 
> solve problems that the computer cannot solve for itself.

Also many halting problems can be "solved" by finding a weak point and 
changing the problem.  That may sound like cheating, but it is still 
very useful.

For example, software code verifiers trying to prove if a piece of code 
"halts" or not cannot do it for arbitrary input.  But it can suggest to 
the programmer, "Hey, put a contract/assert here to limit the range of 
inputs and then I can prove it."

for(i=0; i<x; i++) { print i } for unknown x may never halt, but:

assert(x >= 0 && x < 1000)
for(i=0; i<x; i++) { print i } will provably halt at 1000 or sooner.

There are similar fixes for other classes of problems where the fixes 
are not necessarily pretty or elegant but result in answers that work 
well enough in the real world.
-- 
Zan Lynx
zlynx at acm.org

"Knowledge is Power.  Power Corrupts.  Study Hard.  Be Evil."