Neil Mitchell wrote: >> 1) The programmer has to detail in some form the proof that his program >> terminates. Arguably, he ought to do so anyway but he doesn't need to >> write his proof in a way that can be checked by a dumb computer. Take >> for example >> >> minimum = head . sort > > minimum [1..] gives _|_ non-termination > > miniumum [1,_|_,3] gives _|_ while head [1,_|_,3] doesn't. > > Termination is all a bit more complex once you get to laziness.
Oops, the example was not meant for termination but for the invariants. I wanted to say that the code of minimum is likely to be shorter than a computer-checkable proof that shows that its result is indeed the smallest element from the list. Regards, apfelmus _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
