Static checking

First, my background: I am seeking my Master's degree in Computer Science after procuring a Bachelor's in the same field. I have worked in the IT industry as a "consultant" (glorified sysadmin) and also as a student aid (grader) and researcher (kernel hacker) while pursuing my education--that is, I tend to work more than I attend school and am entering my eighth year of higher education. That is all to say I have never worked in "industry" as a programmer, only in acadamia as a programmer, but I have done some light programming in conjunction with administration.

This means that I have had it hammered into my head by professors for the last 6 years or so that I've been taking classes in my subject that static checking (often referred to has "type checking") is the most important aspect (or one of the most important aspects) of a computer language. However, I've always been a bit skeptical of this view since static checking only buys a couple minor things while robbing you blind of many things.

I even took a class on static checking which was wrapped tightly around Pierce's text Types and Programming Languages. One of the major bits of this text is it's creation of a mini-Java language (FJ), which is provably type-safe. However, the proof uses a hack to make sure that downcasts (e.g., casting from Object to anything else) is actually "safe". Therefore, I've begun to reach the opinion that "there is no free lunch" when it comes to static checking. Static checking only guarantees that our programs are sort-of-kind-of safe so long as we're careful and the exception handling system is leveraged properly. In Java, in particular, you can throw type safety completely away by introducing any code using reflection, but it is a necessity in some areas--try writing a J2EE container without reflection!

Simply guaranteeing that a function returns an int when it claims to does not come anywhere close to guaranteeing that it is the right value (woo-hoo, I've limited the number of results to 4-billion!). Don't misunderstand me as saying static checking is utterly worthless, but simply contemplating it's real value as opposed to what I percieve as the inflated value given to it by some in the language community.

My question to the monks is, how much does static checking buy us and is it really worth the bother at all? Is static checking worth the limitations imposed upon expressiveness? If so, where and why? How useful is static checking in industry (various industries)? I know it's useful for catching typos (so that something like When -w and use strict aren't enough... doesn't happen), but isn't proper testing a much better road to proving the correctness of code? So often, it seems like programmers--especially ones who are susceptible "false laziness"--gain a false sense of security in static checking. (How many of us GTAs have run into early undergrads who say at a low grade on a homework, "But it works, it compiles doesn't it?" Or heck, we're in a hurry to turn something in ourselves, made a small change we know will work, compile it and find out later was totally broken because we skipped actual testing.)

Anyway, since Perl's static checking is limited by it's expressiveness and is turned off by default, I was looking for a Perlish answer (along with any other perspective of this diverse community)..

Comment on Static checking Download Code

Replies are listed 'Best First'.
Re: Static checking by blokhead (Monsignor) on Nov 04, 2003 at 22:25 UTC
I can't think of a better discussion of typing issues than Dominus' Strong Typing and Perl talk. He knows a lot more about programming design than I do. In the talk, he argues that static typing (at least in C) is pretty much a failure. A very interesting alternative he brings up is a type-inferencing language like ML (or its variants). ML is a cool language if you have the chance to learn it, and I can attest to the fact that type inferencing really does help to avoid bugs. In some senses, Perl really is strongly typed... at least in terms of scalars vs compound types. I seem to remember someone's sig around here that has a quote about Perl being strongly typed but not having many types. The best example of this is that a hash or array value must always be a scalar. Of course, Perl gives us references and does things like listification, so we hardly notice the distinction after a while. In the end, I think it's really the polymorphism of the various scalar types (and not the lack of types) that lets us do all the things we love in Perl. blokhead	[reply]
Re: Re: Static checking by hanenkamp (Pilgrim) on Nov 06, 2003 at 19:27 UTC
Actually, I have done quite a bit of class work in SML/NJ and OCAML. However, I can't say that I like the languages much. It's so much structure that I have a hard time knowing what pieces to use to solve a problem. The book I mentioned above discusses language in a very ML-like way. It provides an interesting perspective, but it's too mechanical for being very useful to me in programming.	[reply]
Re: Static checking by hardburn (Abbot) on Nov 04, 2003 at 22:01 UTC
I think you'll find most people here don't like type checking, so this may not be the best place to ask this question. Personally, I can see a use for checking when you're passing around objects, but not primitives like integers and strings. Perl's DWIM is good enough that it'll usually know how to convert one primitive into another transparently, so I don't consider them a problem. However, when you pass in an object, you want to make sure that the methods you call are going to exist. No ammount of DWIM will save you from calling a method that isn't there. ---- I wanted to explore how Perl's closures can be manipulated, and ended up creating an object system by accident. -- Schemer `: () { :\|:& };:` Note: All code is untested, unless otherwise stated	[reply] [d/l]
Re: Static checking by chromatic (Archbishop) on Nov 05, 2003 at 01:06 UTC
I'm of the opinion that type systems as commonly found confuse several things: Compiler optimizations. Memory size and locations. Position in a class hierarchy. Supported behavior. Of those, only the second and fourth have much to do with program correctness. Even then, there are too many other things that can go wrong — suppose you implement the `Serializable` interface in a Java class but code a method body incorrectly. Even static analysis of the code can't catch logic errors. A well-written test suite can catch those kinds of errors. You'll never get around that with a compiler. It's up to you if the price to pay for static types is worth the things it can possibly catch.	[reply] [d/l]
Re: Static checking by fletcher_the_dog (Friar) on Nov 05, 2003 at 16:34 UTC
I may be totally wrong, but I always thought that the advantage of static typing had mostly to do with speed and size. For example in the following sub, every time it runs it has to first look up what type of object $thing is and then check to see if that type of object has a "to_xml" method. `sub foo{ my $thing = shift; print $thing->to_xml; }` [download] But in the following (probably bad) C++ code, the function can be looked up just once at compile time, because the function knows what type of object 'thing' will be: `void foo(bar thing){ cout << thing.to_xml(); }` [download] Yet another layer is added when you use overloading. Let's say that a variable is used in a concatenation, perl must first determine what if any class of object that variable belongs to. If the variable does belong to a class it must determine if that class has the concatentation operator overloaded, if it does then in must determine if the subroutine exists that it is overloaded with, and then it calls that subroutine. In a static typed language this only has to be done once at compile time. The size difference shows most with ints and chars. As I understand it in perl every scalar is a C struct. If a variable is only ever going to be an int, then it is a waste to make a struct for it. I am not saying that static typing is better, but I think there are some speed and size advantages.	[reply] [d/l] [select]
Re: Re: Static checking by hardburn (Abbot) on Nov 05, 2003 at 17:17 UTC
I may be totally wrong, but I always thought that the advantage of static typing had mostly to do with speed and size. Those are often advantages to a type system, but it's also a debugging aid. In your Perl example, what happens if `$thing` is a simple scalar instead of a blessed reference? Or what if it is an object, but that object doesn't implement a `to_xml` method? In Perl5, you won't know these things until runtime. Whereas with the C++ example, the compiler will complain if `thing` isn't a `bar` instance. Though the C/C++ type system is broken in some ways which hurt debugging, which is covered in Dominus' Strong Typing talk (noted earlier in this thread). ---- I wanted to explore how Perl's closures can be manipulated, and ended up creating an object system by accident. -- Schemer `: () { :\|:& };:` Note: All code is untested, unless otherwise stated	[reply] [d/l] [select]