🚀 go-pugleaf

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

I suppose such a thing could be quite instructive.  Ask the question
"how useful is this language when I remove everything which
potentially prevents halting?".  If nothing else, it might tell you
where the language designers were at.

Raul Rockwell