🚀 go-pugleaf

In article <1991May4.192440.5527@sctc.com> beede@sctc.com (Mike Beede) writes:
>yodaiken@chelm.cs.umass.edu (victor yodaiken) writes:
>
>>The halting problem does not really apply to actual programming languages
>>(i.e. those that are compiled or interpreted into machine code).
>>The sooner computer scientists begin to understand the actual meaning
>>of the undecidability and complexity results, the better off the filed
>>will be.
>
>Trivially, this is true.  We can always run the program on the machine
>and look for a cycle in the total state (all memory, all register, all
>etc.)  Then we wait for on the order of 
>
>	2 ^ ( 2 ^ wordsize * ( memorysize + registercount ) ) 
>
>cycles (corrected for any non-binarity of the machine) and if we don't
>get a repeat, the program never halts.  The approximate length of time
>for my workstation (2^23 8-bit bytes, and arbitrary count of 8
>registers, the number really doesn't matter), if it didn't have any
>disk, and assuming 2^24 operations/sec, is 2^8388584 seconds ~=
>2^8388559 years, or something like 10^2,800,000 years.  Net bandwidth
>considerations demand exponential notation for numbers of this size.
>Any even near-reasonable postulated speed increase will have no
>noticible effect on this number (it will still exceed the lifetime of
>the universe by an unreasonable factor).

If the halting problem applied to actual computers, then there would
be no bound on any algorithm to solve the problem. There is an obvious,
although impractical algorithm, however, so the invocation of Turing's
theorem is misplaced. Large numbers are not equal to infinite numbers,
hard problems are not equivalent to impossible problems. If you want to
say that deciding type problems for programing languages is unlikely
because the immense state spaces are not tractable to analysis, then fine.
But, if you want to say that Turing's theorem, or Herbrands theorem,
or Fermats theorem tells us that type checking real programs is 
impossible, then you don't understand any of these theorems ( or you've
figured out something that it would be interesting to hear about).

>I would say that this is close enough to insoluble for government
>work, as the saying goes.  Am I missing something in your post?  I'd

While "hard = insoluble" may be close
enough for government work, it's not true. There may be a wonderful
algorithm out there that in practice can verify type safety of 
very complex programs in a reasonable time. Is there such an
algorithm? I don't know. But I do know that there is no proof
that such an algorithm is impossible.