Luis Zarrabeitia <ky...@uh.cu> writes: > Btw, the correctness of a program (on a turing-complete language) > cannot be statically proven. Ask Turing about it.
Be careful! Given a putative correctness-checking algorithm, there exist programs for which the algorithm gives the wrong answer. That doesn't necessarily mean that there isn't a useful subset of `all programs' which can be proven correct, or even that this subset doesn't include all `interesting' programs. Even so, actually constructing algorithms which prove interesting things about all interesting programs seems difficult. Some people (let's call them `type A programmers') have decided that they want to be assisted with writing correct programs -- to the extent that they've chosen some correctness properties, and use a tool which reject programs that it can't prove have those properties. Since the tool can't work for all programs, it errs on the side of caution, sometimes rejecting correct programs. (The properties tend to be called `type correctness' and the tool is built into the compiler, but that's not actually very important.) Other people (`type B programmers') don't like having their (apparently? possibly?) correct programs rejected. Instead, they'd rather risk writing incorrect programs (maybe they try to minimize the risk by thinking very hard, or by building thorough test suites) because they find that some of the kinds of programs the tools reject are actually interesting and useful -- or at least fun. I think trying to persuade a type A programmer that he wants to work like a type B programmer, or /vice versa/, is difficult, bordering on futile. Type A stereotypes type B as a bunch of ill-disciplined reckless hackers; type B stereotypes type A as killjoy disciplinarians. Meeting in the middle is difficult. (`We just want to add a little safety.' `You want to take away our freedom!' Etc., /ad nauseam/.) On a personal note, I've written programs in lots (/lots/) of different languages: C, Pascal, Haskell, Standard ML, Python, Perl, Lisp, Scheme, and assembler for various processors. I always found programming in permissive languages more enjoyable. I still love ARM assembler (though I thought the 32-bit address space changes spoilt some of its beauty), but I don't get to write much these days; Common Lisp is now my language of choice, but Python comes very close. I find C too fiddly and annoying nowadays, and its type system does an impressive job of simultaneously being uncomfortably constraining while being too weak to provide a satisfactory feeling of confidence in compensation. Kernighan summed up Pascal perfectly when he said `There is no escape.' Haskell is interesting: it can provide a surprising degree of freedom, but it makes you work /very/ hard wrangling its type system in order to get there; and again, I found I had most fun when I was doing extremely evil unsafePerformIO hacking... So, my personal plea. Writing Python is /fun/. Please let it stay that way. -- [mdw] -- http://mail.python.org/mailman/listinfo/python-list