🚀 go-pugleaf

In article <30275@dime.cs.umass.edu> yodaiken@chelm.cs.umass.edu (victor yodaiken) writes:

|Sure. Can it be done in practice, for every language and every program? 
|I'll bet, no. But, there is no theoretical reason why a clever design
|could not produce a useful programming language with a compiler that
|verified termination.  

Well, this minimal condition has of course been met. The language
Brouwer was useful, and its compiler guaranteed termination (it didn't
verify it directly; its type system was based on Intuitionistic Type
Theory, which simply lacks noterminating constructs).

Of course, what Brouwer was useful FOR was merely proving the point
that it could be done <smilie smilie smilie>: it wasn't what you'd
call a _practical_ programming language (it was a bitch to code in and
took forever to compile).

But for all the world it felt INCONVENIENT and underdeveloped rather
than HOPELESS. And that's speaking as someone who counts cycles and
criticises code generators.
----------------------------------------------------------------------
stephen p spackman         Center for Information and Language Studies
systems analyst                                  University of Chicago
----------------------------------------------------------------------