Paul Rubin a écrit : > Bruno Desthuilliers <[EMAIL PROTECTED]> writes: > >>> [A type system is a] tractable syntactic method for proving the >>> absence of certain program behaviors by classifying phrases >>> according to the kinds of values they compute. (Pierce 2002)." >> >>Is this supposed to contradict my assertion that *static* typing is >>for compilers ? > > Yes, the main benefit these days is to prove the absence of certain > types of bugs in the program.
As someone said, if declaring types thrices was enough to ensure correctness, I'd happily do so. I still maintain that the primary *practical* reason behind static typing is to provide optimization clues for the compiler. You can (or at least could) have declarative static typing with very few type *checking* - I may be wrong here but I think one could even write a C compiler without *any* type checking. Heck, the programmer said it's a char*, so it must be one, right ?-) Of course, no one in it's own mind would use such a compiler (if you have to suffer from the restrictions imposed by static typing, you want to also profit from it's benefices - or at least avoid the possibly dramatic effects of a type error in these systems). Also, some (mostly) dynamically typed languages have grown type-annotations for the very same reason : hinting the compiler about possible optimizations. wrt/ proofs of correctness, I'll just point to the spectacular failure of Ariane, which was caused by a *runtime* type error in a system programmed in ADA - one of the languages with the most psychorigid declarative static type systems. Not to say these proofs are inexistant, just that they are IMHO a bit overvalued - at least wrt/ to my daily concerns. Most of the errors I have to deal with are logical errors, not type errors, and given the kind of "logic" (err...) you can find in business applications (to make a long story short : it has very few to do with mathematics), I have some doubt about what a static type system - even a _very_ smart one - could prove here, at least if we hope to deliver the application within time and budget constraints (sorry for being soo practical here). > The article "What To Know Before Debating Type Systems" is pretty > informative (though it doesn't go as far as to call C/C++ untyped): > > http://cdsmith.twu.net/types.html Quote : """ Therefore: I give the following general definitions for strong and weak typing, at least when used as absolutes: * Strong typing: A type system that I like and feel comfortable with * Weak typing: A type system that worries me, or makes me feel uncomfortable """ According to this definition, I herefore declare that Python is strongly typed and Java weakly typed !-) (sorry, couldn't resist). More seriously, it's indeed an interesting article - even if I do not necessarily share all the views of the author - for those not knowing anything about type systems. But it's clearly a bit oriented and IMHO fails to present the pros of dynamic typing. BTW, if I may insert another quote, that I think is relevant here as well as in another recent thread about 'typed' containers in Python: """ I find it amusing when novice programmers believe their main job is preventing programs from crashing. I imagine this spectacular failure argument wouldn't be so appealing to such a programmer. More experienced programmers realize that correct code is great, code that crashes could use improvement, but incorrect code that doesn't crash is a horrible nightmare. """ > >>>C and C++ are basically untyped languages. >> >>Hem... This assertion is at least debatable. Care to post this on >>c.l.c or c.l.c++, so we get some feedback ? > > I wouldn't consider the aficionados of those dinosaur languages Hmmm... For a dinausor, C seems well alive. Can you remind me which language is used to implement CPython and most of actual operating systems and low-level libraries ? > to be > authorities on such a question. If you mean that most them aren't necessarily great CS theorists, then you may be right. OTHO, they do have some practical experience with these languages, so they might have something to say... -- http://mail.python.org/mailman/listinfo/python-list
