🚀 go-pugleaf

In article <ROCKWELL.91May14081634@socrates.umd.edu> rockwell@socrates.umd.edu (Raul Rockwell) writes:
>
>   >Victor Yodaiken:
>   >>But, there is no theoretical reason why a clever design could not
>   >>produce a useful programming language with a compiler that
>   >>verified termination.
>
>   David A. Truesdell:
>   >The answer to the question is "NO".  It is not possible in
>   >practice, it is not possible in theory.
>
>Joseph Allen:
>   No, it can be done!  Really!  Just don't allow loops, gotos or
>   recursion.  Now who wants to write a compiler in a language with
>   these restrictions?
>
>Well, you can allow loops as long as they can guaranteed to be
>bounded.  And you don't really need a new compiler, just take an
>existing one and remove anything which allows unbounded loops or
>recursion.
>

The kind of looping that makes Turing machines undecidable is quite
different from the kind of looping we get in real machines. On
a turing machine
            while(true)i = i+1;
is a truly infinite loop, each iteration takes us to a new state.
But on a real computer, 
            while(true)i = i+1;
*will* repeat state (or crash the program). Here we have a *finite* loop.

Similarly, bounded recursion, even with implicit bounds, is all we have
on real computers -- eventually stacks will overflow. So it is, in
principle, quite possible to write an ANSI "C" compiler that would
detect non-terminating loops. The compiler would have to know someting
about the limits of adressable memory onthe machine, but, that does not
seem unreasonable.