Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cs.utexas.edu!uunet!stealth.acf.nyu.edu!brnstnd From: brnstnd@stealth.acf.nyu.edu Newsgroups: comp.software-eng Subject: Re: Have *YOU* ever written a program which COULDN'T be proven correct? Message-ID: <3803:04:53:29@stealth.acf.nyu.edu> Date: 14 Feb 90 04:53:30 GMT References: <7598@hubcap.clemson.edu> <9630012@hpirs.HP.COM> <17080@duke.cs.duke.edu> <789@arc.UUCP> <17143@duke.cs.duke.edu> <793@arc.UUCP> Reply-To: brnstnd@stealth.acf.nyu.edu (Dan Bernstein) Distribution: usa Organization: IR Lines: 17 In article <793@arc.UUCP> steve@arc.UUCP (Steve Savitzky) writes: > I think you missed my point, which is that whether or not the halting > problem can be solved *in theory* for real programs on real computers, > it cannot be solved *in practice*. A year ago I posted a short note to comp.theory titled Finite Halting Problem Considered Solvable. The gist of it is that you can solve the halting problem for a program using just twice the memory and thrice the time. In practice, with language support, you designate certain variables to be tested for looping. Those variables are stored twice, and the program runs at a third of the speed. If those variables together enter a loop, the loop will be detected during its first period. For some programs this could be very useful. ---Dan