On Thursday 12 February 2009 16:19:55 Michael G Schwern wrote: > chromatic wrote:
> > Why? It would be practically useless unless they proved all cases of > > input (user and hardware), in which case it would only be practically > > useless for every case which lacks complete proofs. > I'm no expert, but I'm given to understand this exactly the problem Monads > were developed to deal with. I think you're thinking of type systems, and those only work if they're sufficiently expressive enough to prove characteristics of your program sufficient to describe what you need to do, and provided you choose the right types. It's trivial to write a type-safe Haskell program which does not violates mathematical laws tought to fifth graders and which never terminates. I can do it in fewer than ten lines of code. Does that make Haskell useless? Type systems? Theorem proving? No -- but it proves that they're not sufficient. -- c
