Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!mips!pacbell.com!att!linac!midway!midway!stephen From: stephen@estragon.uchicago.edu (Stephen P Spackman) Newsgroups: comp.lang.misc Subject: Re: Halting Problem Solved! Film at 11! (Was Re: definitions) Message-ID: Date: 9 May 91 08:34:59 GMT References: <30040@dime.cs.umass.edu> <30275@dime.cs.umass.edu> Sender: news@midway.uchicago.edu (NewsMistress) Organization: University of Chicago CILS Lines: 24 In-Reply-To: yodaiken@chelm.cs.umass.edu's message of 8 May 91 23: 01:52 GMT 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 : 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 ----------------------------------------------------------------------